| Table of Subpages |
|---|
 |  |
 |
Overview
From this page, you will find analysis tools for various classes of problems, mostly in systems analysis. There are tools using techniques in theorem proving, model checking, computer algebra, verification of hybrid systems. Some other parts center around artificial intelligence and heuristic search, parser technology, or object-orientation. Some of these algorithms are implemented in the Orbital library.
Verification tools:
- KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (new)
- KeYmaera 3: A Theorem Prover for Hybrid Systems (previous generation)
- KeYmaeraD for distributed hybrid systems
- AMC
- SAAtRe
- j'Imp Prover