Skip to Main Content Area
CPS-VO
Contact Support
› Go to login screen
Not a member?
Click here to register!
Forgot username or password?
Verification Tool Library
Home
README
Search for Tools
Browse Tool Library
Members
Tutorials
Tutorial - SpaceEx
Files
CPS-VO
»
CPS Tools and Design Studios
»
Verification Tool Library
» OWN LANGUAGE
Own language
wikipage
UPPAAL
Submitted by akarns on Mon, 05/08/2017 - 10:09am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Mac OS X
Windows
Network of timed automata
Timed automata abstractions
Guaranteed to terminate
Schedulability analysis
Synthesis
wikipage
PHAVer
Submitted by akarns on Mon, 05/08/2017 - 10:04am
Validation and Verification
Free
Own language
Linux
Mac OS X
Windows
Piecewise affine hybrid systems
Overapproximations of piecewise affine dynamics
Guaranteed to terminate
Reachability analysis
wikipage
SpaceEx
Submitted by akarns on Mon, 05/08/2017 - 10:02am
Validation and Verification
Tool
Free
Own interface
Own language
Systems encoded in XML files
Linux
Mac OS X
Windows
Hybrid systems with piecewise constant bounds on the derivatives
Linear hybrid systems with nondeterministic input
Flowpipe overapproximations
Polyhedral representations and approximations
Set clustering methods
Support functions
Not guaranteed to terminate
Reachability analysis
wikipage
PRISM
Submitted by akarns on Mon, 05/08/2017 - 9:52am
Validation and Verification
Tool
Free
Own interface
Own language
Linux
Mac OS X
Windows
Continuous-time Markov chains
Discrete-time Markov chains
Discrete/continuous and deterministic/nondeterministic probabilistic models
Markov decision processes
Probabilistic automata
Probabilistic timed automata
Quantitative abstraction refinement
Guaranteed to terminate
Probabilistic model checking
wikipage
Kronos
Submitted by admin on Tue, 02/28/2017 - 5:10pm
Validation and Verification
Tool
Free
Own language
Linux
Windows
Network of timed automata
Abstractions
On-the-fly model checking
Syntactic optimization
Guaranteed to terminate
Model checking
wikipage
KeYmaera X
Submitted by Andre Platzer on Tue, 02/28/2017 - 5:09pm
Validation and Verification
Tool
Free
Own interface
Own language
Linux
Mac OS X
Windows
(Event-triggered) polynomial hybrid systems
Compositional verification
Differential dynamic logic
Not guaranteed to terminate
Theorem proving
wikipage
KeYmaera
Submitted by Andre Platzer on Tue, 02/28/2017 - 5:07pm
Validation and Verification
Tool
Free
Own interface
Own language
Linux
Mac OS X
Windows
(Event-triggered) polynomial hybrid systems
Distributed polynomial hybrid systems
Compositional verification
Differential dynamic logic
Not guaranteed to terminate
Theorem proving
wikipage
FLOW*
Submitted by admin on Mon, 02/27/2017 - 2:32pm
Validation and Verification
Tool
Free
Own language
Linux
Mac OS X
Windows
Linear Hybrid Systems
Linear Systems
Nonlinear hybrid systems
Nonlinear hybrid systems with bounded time-varying uncertainties
Nonlinear systems
Flowpipe overapproximations
Set clustering methods
Taylor models
Guaranteed to terminate
Reachability analysis
wikipage
d/dt
Submitted by admin on Tue, 02/21/2017 - 4:14pm
Validation and Verification
Tool
Contact the author
Own language
Linear hybrid systems with nondeterministic input
Under approximations of maximal invariant sets
Polyhedral representations and approximations
Guaranteed to terminate
Reachability analysis
« first
‹ previous
1
2
