Tools for Logic, Computer Science & Mathematics

Table of Subpages

KeYmaera: A Hybrid Theorem Prover for Hybrid Systems
Case Study: European Train Control System
Case Study: Formal Verification of Curved Flight Collision Avoidance Maneuvers
Case Study: Distributed Adaptive Cruise Control
Case Study: Mobile Robots and Surgical Robots
Sphinx: Verification-Driven Engineering Toolkit
KeYmaeraD: Distributed Theorem Prover for Distributed Hybrid Systems
AMC: Approximation Refinement Model Checker
SAAtRe: SAT-based Abstraction Refinement
Orbital library
j'Imp Theorem Prover
j'Abr Computer Algebra System
Synx: Integrated Compiler Construction Kit
Simple Board Games and Visualizations
Download



	$Simple Board Games and Visualizations$

Overview

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:

KeYmaera
KeYmaeraD
AMC
SAAtRe
j'Imp Prover