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…

Latest News

CAV 2013 in St. Petersburg!

Our group is co-organizing CAV 2013, the leading conference in computer-aided verification. The conference will take place July 13-19, 2013, during the famous White Nights in beautiful St. Petersburg.  

Continue reading

Full news archive