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

Facebook group for Austrian computer scientists

There is a new facebook group for communication among Austrian computer scientists: https://www.facebook.com/groups/AustrianComputerScience/ For those who are skeptical about facebook, we created a read-only mirror (beta version): http://forsyte.at/acs/  

Continue reading

Johannes Kinder joins Royal Holloway

After a postdoc with George Candea, FORSYTE alumnus Johannes Kinder will start a lecturer position at Royal Holloway in September 2013! Congratulations! http://people.epfl.ch/johannes.kinder?lang=en&cvlang=

Continue reading

Full news archive