Software
The FORSYTE group provides and maintains a number of (research) software projects. Detailed information, including downloads and publications can be found on the respective tool's page.
- APALACHE: Abstraction-based parameterized TLA+ model-checking.
- ByMC: Parameterized model-checking of fault-tolerant distributed algorithms.
- COACHMAN: Complexity analyzer for concurrent heap-manipulating programs.
- TMCA: Thread-modular counter abstraction for parameterized program safety.
- Vampire: First-order superposition-based automated theorem prover.
Former Projects
- CMBC-GC: Compiling C programs for secure two-party computation.
- ConCREST: Concolic testing tool of multi-threaded C programs.
- CPA/Tiger: Predicate-abstraction based test input generator for C programs.
- FShell: Testing environment for C programs, designed as a database engine dispatching queries about the program to program analysis tools.
- iDQ: Instantiation-based DQBF (Dependency Quantified Boolean Formula) solver.
- Loopus: Symbolic bound computation for loops in C Programs.
- Verifolio: Machine learning-based portfolio software verification tool.