Software tools discussed in the course
- Z3: SMT Solver
- α,β-CROWN: Neural network verifier based on bound propagation + branch and bound
- PVS : A general-purpose theorem prover for higher order logic.
- SpaceEx: Another model checker for Hybrid Systems
- UPPAAL : A model checker for timed systems
- C2E2: Nonlinear hybrid system verification tool
- DryVR: Model-free verification
Related tools and benchmarks
- ARCH competition publishes dozens of benchmarks; you can submit!
- VNN competition: Verification of Neural Networks Competition
- Flow*: Nonlinear hybrid reachability analysis tool
- PHAVER: A model checker for Hybrid Systems
- HyST: model-to-model transformer
- Enormous list of tools
See this page for help with installing and running some tools