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. Read more…
- ByMC: Parameterized model-checking of fault-tolerant distributed algorithms. Read more…
- COACHMAN: Complexity analyzer for concurrent heap-manipulating programs. Read more…
- TMCA: Thread-modular counter abstraction for parameterized program safety. Read more…
Former Projects
- CBMC-GC: Compiling C programs for secure two-party computation. Read more…
- ConCREST: Concolic testing tool of multi-threaded C programs. Read more…
- CPA/Tiger: Predicate-abstraction based test input generator for C programs. Read more…
- FShell: Testing environment for C programs, designed as a database engine dispatching queries about the program to program analysis tools. Read more…
- iDQ: Instantiation-based DQBF (Dependency Quantified Boolean Formula) solver. Read more..
- Loopus: Symbolic bound computation for loops in C Programs. Read more…
- Verifolio: machine learning-based portfolio software verification tool. Read more…