Tools for Logic, Computer Science & Mathematics

KeYmaera: A Hybrid Theorem Prover for Hybrid SystemsOrbital library
Sphinx: Verification-Driven Engineering ToolkitSimple Board Games and Visualizations
SAAtRe: SAT-based Abstraction RefinementSynx: Integrated Compiler Construction Kit


From this page, you will find tools, mostly associated with algorithms from logic in computer science. 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. A lot of practical results and algorithms in these areas of computer science are contained in the Orbital library.

Verification tools: