Resources

The CPS book page

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