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
» GUARANTEED TO TERMINATE
Guaranteed to terminate
wikipage
TuLiP
Submitted by akarns on Mon, 05/08/2017 - 10:41am
Validation and Verification
Tool
Free
Python
Linux
Mac OS X
Windows
Piecewise affine hybrid systems
Abstractions
Digital Design Synthesis
Receding Horizon Planning
Guaranteed to terminate
Synthesis
wikipage
C2E2
Submitted by akarns on Mon, 05/08/2017 - 10:37am
Validation and Verification
Tool
Free
Own interface
Own language
Linux
Nonlinear hybrid systems
On-the-fly Discrepancy Computation
Overapproximations
Reach Tubes
Guaranteed to terminate
Model checking
wikipage
UPPAAL STRATEGO
Submitted by akarns on Mon, 05/08/2017 - 10:14am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Windows
Priced timed automata
Stochastic timed automata
Statistical techniques
Timed automata abstractions
Guaranteed to terminate
wikipage
UPPAAL CORA
Submitted by akarns on Mon, 05/08/2017 - 10:13am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Mac OS X
Windows
Linear priced timed automata
Timed automata abstractions
Guaranteed to terminate
Cost optimal reachability analysis
wikipage
UPAAL SMC
Submitted by akarns on Mon, 05/08/2017 - 10:12am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Mac OS X
Windows
Priced timed automata
Statistical techniques
Timed automata abstractions
Guaranteed to terminate
Statistical model checking
wikipage
UPPAAL Times Tool
Submitted by akarns on Mon, 05/08/2017 - 10:11am
Validation and Verification
Tool
Free
Model editor integrated
Own language
Linux
Mac OS X
Windows
Network of timed automata extended with tasks
Timed automata abstractions
Guaranteed to terminate
Schedulability analysis
Synthesis
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
SCOTS
Submitted by akarns on Mon, 05/08/2017 - 10:06am
Validation and Verification
Tool
Free
Matlab
Linux
Mac OS X
Nonlinear perturbed control systems
Abstractions
Guaranteed to terminate
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
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
« first
‹ previous
1
2
3
4
5
next ›
last »
