Software

This page list software provided and maintained by the FORSYTE group. Detailed information, including downloads and publications can be found on the respective tool’s page:

• ByMC

  ByMC is a parameterized model checker of fault-tolerant distributed algorithms. Read more…

• Loopus

  A Tool for Computing Symbolic Bounds on Loops in C Programs. Read more…

• Verifolio

  Verifolio is a machine learning-based portfolio software verification tool. Read more…

• CBMC-GC

  CBMC-GC is a compiler for C programs in the context of secure two-party computation. Read more…

• ConCREST

  ConCREST is a concolic testing tool for multi-threaded C programs. Read more…

• CPA/Tiger

  CPA/Tiger is a predicate-abstraction based test input generator for C programs. Read more…

• FShell

  FShell provides a versatile testing environment for C programs which supports both interactive explorative use and a rich scripting language. More than a frontend for software model checkers, FShell is designed as a database engine which dispatches queries about the program to program analysis tools. Read more…

• Diagnostics

  Diagnostics is a unified framework for code annotation, logging, program monitoring, and unit-testing. Read more…

• Hessen Automata Library

  A library for automata and regular expression manipulation. Read more…

• iDQ

  iDQ is an instantiation-based DQBF (Dependency Quantified Boolean Formula) solver. Read more…