2LS ("tools") is a verification tool for C programs, built upon the CPROVER framework. It allows one to verify user-specified assertions, undefined behaviour, memory leaks, and termination properties. The analysis is performed by translating the verification task into a second-order logic formula over bitvector, array, and floating-point arithmetic theories. The formula is solved by a modular combination of algorithms involving unfolding and template-based invariant synthesis with the help of incremental SAT solving.
AISE is a software verifer that verifes C programs with respect to reachability properties. The key idea of AISE is to synergize symbolic execution (SE) and abstract interpretation (AI).
AProVE (KoAT + LoAT) is a system for automated termination proofs for C / LLVM programs. To (dis)prove termination of C programs, AProVE uses symbolic execution to transform the program's LLVM code into an integer transition system (ITS). These ITSs are analyzed by our backend tools KoAT (for termination) and LoAT (for non-termination).
CADP is a verification toolbox developed initially at Verimag, then at INRIA Grenoble. It provides compilers for concurrent languages (message-passing communication), as well as tools for model checking (value-passing modal mu-calculus), equivalence checking (bisimulations and behavioural preorders), simulation, and test-case generation. The first version of CADP was released in 1989.
ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both data-nondeterminism and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness.
CoVeriTest is a test-case generation approach based on the analysis framework CPAchecker. It mainly uses verification techniques to detect the (un)reachability of test goals and generates test cases from the counterexamples to unreachability of the test goals. More concretely, it is a hybrid approach that interleaves expicit value analysis and predicate analysis to check the reachability of test goals.
CPA-witness2test is an execution-based validator for violation witnesses on C programs. It derives a test case from a violation witness and executes the input program on the derived test case. If CPA-witness2test observes that the execution triggers a property violation, then the witness under validation is confirmed.
CPAchecker is a configurable framework for software verification that is based on configurable program analysis and implements many model-checking algorithms to check for software errors and to verify program properties.
Deagle is an partial-order-based bounded model checker for concurrent program verification. It is built on top of CBMC-5 (front-end) and MiniSAT-2.2.1 (back-end), majorly enhancing them with an ordering consistency theory which handles ordering relations over shared memory accesses in concurrent programs.
EmergenTheta is a variant of Theta utilizing emerging techniques previously missing from Theta. We step away from Theta's conventional, abstraction-based techniques and use a portfolio of BMC, IMC, k-induction, and saturation based techniques, with possible implicit predicate abstraction.
Fizzer is a gray-box fuzzer focussing on coverage of atomic Boolean expressions (mainly the instructions for number comparison). It uses dynamic taint-flow analysis and local space fuzzing (gradient descent, bit and random mutations performed in local spaces).
FuSeBMC is an award-winning automated software testing tool that integrates Bounded Model Checking (BMC), Fuzzing, and Artificial Intelligence (AI) to enhance software security and reliability. Designed to detect and repair security vulnerabilities in C programs, FuSeBMC improves code quality while reducing false positives and operational disruptions.
Goblint is an abstract interpretation framework that is dedicated to the sound thread-modular analysis of multi-threaded programs, especially for data races.
Hornix is a software-verification tool based on the LLVM framework, aiming to verify C/C++ code by employing a custom LLVM pass on the LLVM IR level. It transforms the LLVM IR into a system of constrained Horn clauses (CHC) and uses Z3 to decide about its satisfiability.
JBMC is an open-source SAT- and SMT-based bounded model checking tool for verifying Java bytecode. JBMC can be used to verify or falsify functional properties and show the absence or presence of runtime errors. JBMC relies on an operational model of the Java libraries optimized for program analysis.
KeY is a tool for deductive verification to prove the correctness of Java programs.
Korn is a software verifier for the C programming language. It translates the input program to a representation with constrained Horn clauses (CHCs) and uses off-the-shelf solvers to find loop invariants and function summaries.
LIV is a witness validator that splits the input program into straight-line programs based on the rules of hoare logic. It tries to prove or refute the invariants provided in the input correctness witnesses based on the straight-line programs.
MetaVal is an annotation-based witness validator that uses an 'off-the-shelf' verifier to re-establish the verification result using a program expressing the product automaton of the witness and input program. From the verification verdict of the product program the witness validation verdict is obtained.
MetaVal++ is the successor of MetaVal. It validates witnesses by transforming a validation task (a specification, a program, and a verification witness) into a validation or verification task. MetaVal++ provides multiple different frontends for the task transformation. Each produced task can then be verified using multiple verification backends.
Nacpa is a meta-verifier for C programs. It is based on strategy selection, parallel portfolios, and native compilation of Java.
PRISM is a probabilistic model checker. It has been developed and maintained at Oxford University over the past 25 years. At its core, the tool supports formal modeling and analysis of systems with random or probabilistic behavior, and it can analyze a wide spectrum of models based on Markov chains and probabilistic automata.
PRTest is a plain random black-box test-case generator that uses random generation of input values and coverage checks to find input values that improve the coverage. The purpose of PRTest is to provide a base line for performance evaluation of test-generation tools, and therefore, it does not employ any complementing techniques, such as symbolic reasoning or evolutionary algorithms.
RacerF is a static analyser for detection of data races in multithreaded C programs implemented as a plugin of the Frama-C platform. The tool is based on a combination of under- and over-approximation techniques to provide fast and scalable analysis, without sacrificing too much precision.
SVF-SVC is an SV-COMP compatibility wrapper around the Static Value-Flow Analysis Framework (SVF) which leverages sparse and on-demand analysis to check for software vulnerabilities and verify program invariants.
Symbiotic is a configurable framework for program analysis and verification combining static analyses, program slicing, and several tools as verification engines, in particular (a fork of) Klee and Slowbeast.
Symbiotic-Witch is a tool validating violation witnesses of verification results in the witness format 1.0. The tool uses some components of Symbiotic and (a fork of) Klee.
Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. We utilize our portfolio with dynamic algorithm selection to guide configuration synthesis and ordering, thus providing an automatic, adaptive verification solution.
Thorn is a variant of Theta, utilizing CHC solvers as backends instead of the conventional model checking algorithms of Theta.
TracerX is a dynamic symbolic executor that uses interpolation to prune subtrees whose traversal is no longer necessary due to their similarity with previously visited paths.
TracerX-WP is a dynamic symbolic execution engine that employs abstraction learning to prune subtrees which are not necessary for traversal, based on their similarity to previously explored paths. It leverages Weakest Precondition interpolation to represent the learned abstractions effectively.
Ultimate Automizer is a software model checker that is based on automata-based techniques and interpolation to check for software errors and to verify program properties.
GemCutter is a verifier for concurrent programs based on commutativity, i.e., the observation that for certain statements from different threads, the execution order does not matter. It integrates partial order reduction algorithms (that take advantage of commutativity) with a trace abstraction-based CEGAR scheme.
Kojak analyses programs using an extension of the Lazy Interpolants CEGAR scheme.
Ultimate Referee is a correctness witness validator.
Ultimate Taipan checks if a program satisifes some safety property by combining trace abstraction with abstract interpretation. Instead of only generating proofs from single traces with an SMT solver, it also uses an abstract interpreter applied to the path program induced by a trace. For concurrency, it uses an explicit product of finite automata.
Ultimate TestGen is a tool for automatic test-case generation. It checks the (un)reachability of test goals and generates test cases from counterexamples by extending trace abstraction with error automata.
Witch is a tool validating violation witnesses of verification results in the witness format 2.0. The tool uses some components of Symbiotic and (a fork of) Klee.
WitnessLint is a simple witness validator that rejects only witnesses that do not adhere to the witness format specification. It does this through syntactic checks of the verification witnesses. It is used by the competition SV-COMP to 'desk-reject' witnesses that do not adhere to the format specification, such that invalid witnesses do not yield points in the competition.
WitnessMap is a simple tool with the same input and output as a verifier that only copies witnesses contained in validation tasks to its output folder. It is used by SV-COMP to place existing verification witnesses at the location where the competition infrastructure expects them (this way, the witness is technically 'produced' by a tool with the same interface as a verifier).