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.
Safety Verification and Refutation by k-Invariants and k-Induction. 2015.
DOI: 10.1007/978-3-662-48288-9_9
2LS for Program Analysis (Competition Contribution). 2016.
DOI: 10.1007/978-3-662-49674-9_56
Bit-Precise Procedure-Modular Termination Analysis. 2018.
DOI: 10.1145/3121136
2LS: Memory Safety and Non-termination - (Competition Contribution). 2018.
DOI: 10.1007/978-3-319-89963-3_24
2LS: Heap Analysis and Memory Safety (Competition Contribution). 2020.
DOI: 10.1007/978-3-030-45237-7_22
2LS: Arrays and Loop Unwinding (Competition Contribution). 2023.
DOI: 10.1007/978-3-031-30820-8_31
2LS for Program Analysis. 2023.
DOI: 10.48550/arXiv.2302.02380
Template-Based Verification of Array-Manipulating Programs. 2024.
DOI: 10.1007/978-3-031-56222-8_12
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).
The software model checker Blast. 2007.
DOI: 10.1007/s10009-007-0044-z
Predicate Analysis with BLAST 2.7 (Competition Contribution). 2012.
DOI: 10.1007/978-3-642-28756-5_39
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.
OPEN/CÆSAR: An open software architecture for verification, simulation, and testing. 2006.
DOI: 10.1007/BFb0054165
Efficient Diagnostic Generation for Boolean Equation Systems. 2007.
DOI: 10.1007/3-540-46419-0_18
Compiler Construction Using LOTOS NT. 2007.
DOI: 10.1007/3-540-45937-5_3
Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. 2007.
DOI: 10.1007/3-540-46002-0_20
Compositional Verification Using SVL Scripts. 2007.
DOI: 10.1007/3-540-46002-0_33
A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. 2010.
DOI: 10.1007/3-540-36577-X_7
BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. 2010.
DOI: 10.1007/978-3-540-31980-1_42
DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. 2006.
DOI: 10.1007/11691372_30
Hierarchical Adaptive State Space Caching Based on Level Sampling. 2009.
DOI: 10.1007/978-3-642-00768-2_21
Smart Reduction. 2011.
DOI: 10.1007/978-3-642-19811-3_9
CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. 2011.
DOI: 10.1007/978-3-642-19835-9_33
Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems. 2012.
DOI: 10.1007/978-3-642-28756-5_11
PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus. 2013.
DOI: 10.1007/978-3-642-36742-7_14
TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation. 2018.
DOI: 10.1007/978-3-319-89963-3_13
Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities. 2020.
DOI: 10.1007/978-3-030-45237-7_4
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.
Software Verification with CPAchecker 3.0: Tutorial and User Guide. 2024.
DOI: 10.1007/978-3-031-71177-0_30
CPAchecker: A Tool for Configurable Software Verification. 2011.
DOI: 10.1007/978-3-642-22110-1_16
A Unifying View on SMT-Based Software Verification. 2018.
DOI: 10.1007/s10817-017-9432-6
CPAchecker 2.3 with Strategy Selection (Competition Contribution). 2024.
DOI: 10.1007/978-3-031-57256-2_21
CPA-RefSel: CPAchecker with Refinement Selection (Competition Contribution). 2016.
DOI: 10.1007/978-3-662-49674-9_59
CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution). 2015.
DOI: 10.1007/978-3-662-46681-0_34
CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution). 2014.
DOI: 10.1007/978-3-642-54862-8_27
CPAlien: Shape Analyzer for CPAchecker (Competition Contribution). 2014.
DOI: 10.1007/978-3-642-54862-8_28
CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution). 2013.
DOI: 10.1007/978-3-642-36742-7_45
Block Abstraction Memoization for CPAchecker (Competition Contribution). 2012.
DOI: 10.1007/978-3-642-28756-5_41
CPAchecker with Adjustable Predicate Analysis (Competition Contribution). 2012.
DOI: 10.1007/978-3-642-28756-5_40
Portability Analysis for Weak Memory Models PORTHOS: One Tool for all Models. 2017.
DOI: 10.1007/978-3-319-66706-5_15
BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. 2019.
DOI: 10.1007/978-3-030-25540-4_19
Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). 2020.
DOI: 10.1007/978-3-030-45237-7_24
Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution). 2021.
DOI: 10.1007/978-3-030-72013-1_26
Dartagnan: SMT-based Violation Witness Validation (Competition Contribution). 2022.
DOI: 10.1007/978-3-030-99527-0_24
CAAT: consistency as a theory. 2022.
DOI: 10.1145/3563292
Static Analysis of Memory Models for SMT Encodings. 2023.
DOI: 10.1145/3622855
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.
FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution). 2021.
DOI: 10.1007/978-3-030-71500-7_19
FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs. 2021.
DOI: 10.1007/978-3-030-79379-1_6
FuSeBMC v4: Smart Seed Generation for Hybrid Fuzzing: (Competition Contribution). 2022.
DOI: 10.1007/978-3-030-99429-7_19
FuSeBMC_IA: Interval Analysis and Methods for Test Case Generation: (Competition Contribution). 2023.
DOI: 10.1007/978-3-031-30826-0_18
FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis. 2024.
DOI: 10.1145/3665337
GDart: an ensemble of tools for dynamic symbolic execution on the Java virtual machine (competition contribution). 2022.
DOI: 10.1007/978-3-030-99527-0_27
SPouT: Symbolic Path Recording During Testing - A Concolic Executor for the JVM. 2022.
DOI: 10.1007/978-3-031-17108-6_6
Goblint is an abstract interpretation framework that is dedicated to the sound thread-modular analysis of multi-threaded programs, especially for data races.
Static race detection for device drivers: the Goblint approach. 2016.
DOI: 10.1145/2970276.2970337
Goblint Validator: Correctness Witness Validation by Abstract Interpretation (Competition Contribution). 2024.
DOI: 10.1007/978-3-031-57256-2_17
Goblint: Abstract Interpretation for Memory Safety and Termination (Competition Contribution). 2024.
DOI: 10.1007/978-3-031-57256-2_25
Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution). 2023.
DOI: 10.1007/978-3-031-30820-8_34
Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution). 2021.
DOI: 10.1007/978-3-030-72013-1_28
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.
A Bounded Model Checking Tool for Verifying Java Bytecode. 2018.
DOI: 10.1007/978-3-319-96145-3_10
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution). 2019.
DOI: 10.1007/978-3-030-17502-3_17
JBMC: A Bounded Model Checking Tool for Java Bytecode. 2023.
DOI: 10.48550/arXiv.2302.02381
KeY is a tool for deductive verification to prove the correctness of Java programs.
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY. 2020.
DOI: 10.1007/978-3-030-64354-6
Deductive Software Verification - The KeY Book - From Theory to Practice. 2016.
DOI: 10.1007/978-3-319-49812-6
The KeY Platform for Verification and Analysis of Java Programs. 2014.
DOI: 10.1007/978-3-319-12154-3_4
The KeY Tool. 2005.
DOI: 10.1007/s10270-004-0058-x
The KeY Approach: Integrating Object Oriented Design and Formal Verification. 2000.
DOI: 10.1007/3-540-40006-0_3
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.
Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer. 2020.
DOI: 10.1007/978-3-030-41600-3_1
Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution). 2023.
DOI: 10.1007/978-3-031-30820-8_37
Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution). 2024.
DOI: 10.1007/978-3-031-57256-2_26
Nacpa is a meta-verifier for C programs. It is based on strategy selection, parallel portfolios, and native compilation of Java.
PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution). 2020.
DOI: 10.1007/978-3-030-45237-7_30
Predator Shape Analysis Tool Suite. 2016.
DOI: 10.1007/978-3-319-49052-6_13
Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution). 2016.
DOI: 10.1007/978-3-662-49674-9_66
Predator Hunting Party (Competition Contribution). 2015.
DOI: 10.1007/978-3-662-46681-0_40
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.
PRISM: A Tool for Automatic Verification of Probabilistic Systems. 2006.
DOI: 10.1007/11691372_29
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation. 2007.
DOI: 10.1007/3-540-46419-0_27
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. 2007.
DOI: 10.1007/3-540-46002-0_5
PRISM 4.0: Verification of Probabilistic Real-Time Systems. 2011.
DOI: 10.1007/978-3-642-22110-1_47
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. 2010.
DOI: 10.1007/978-3-540-24730-2_4
Quantitative Multi-objective Verification for Probabilistic Systems. 2011.
DOI: 10.1007/978-3-642-19835-9_11
Automatic Verification of Competitive Stochastic Systems. 2012.
DOI: 10.1007/978-3-642-28756-5_22
PRISM-games: A Model Checker for Stochastic Multi-Player Games. 2013.
DOI: 10.1007/978-3-642-36742-7_13
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 10: Lazy Memory Initialization and Compact Symbolic Execution (Competition Contribution). 2024.
DOI: 10.1007/978-3-031-57256-2_29
Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding (Competition Contribution). 2022.
DOI: 10.1007/978-3-030-99527-0_32
Symbiotic 8: Parallel and Targeted Test Generation (Competition Contribution). 2021.
DOI: 10.1007/978-3-030-71500-7_20
Symbiotic 8: Beyond Symbolic Execution (Competition Contribution). 2021.
DOI: 10.1007/978-3-030-72013-1_31
Symbiotic 7: Integration of Predator and More (Competition Contribution). 2020.
DOI: 10.1007/978-3-030-45237-7_31
Symbiotic 6: generating test cases by slicing and symbolic execution. 2021.
DOI: 10.1007/s10009-020-00573-0
Symbiotic 5: Boosted Instrumentation (Competition Contribution). 2018.
DOI: 10.1007/978-3-319-89963-3_29
Symbiotic 4: Beyond Reachability (Competition Contribution). 2017.
DOI: 10.1007/978-3-662-54580-5_28
Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution). 2016.
DOI: 10.1007/978-3-662-49674-9_67
Symbiotic 2: More Precise Slicing (Competition Contribution). 2014.
DOI: 10.1007/978-3-642-54862-8_34
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution). 2013.
DOI: 10.1007/978-3-642-36742-7_50
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 Taipan and Race Detection in Ultimate (Competition Contribution). 2023.
DOI: 10.1007/978-3-031-30820-8_40
Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions (Competition Contribution). 2020.
DOI: 10.1007/978-3-030-45237-7_32
Loop invariants from counterexamples. 2017.
DOI: 10.1007/978-3-319-66706-5_7
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.
Test-Case Generation with Automata-Based Software Model Checking. 2024.
DOI: 10.1007/978-3-031-66149-5_14
Refining CEGAR-Based Test-Case Generation with Feasibility Annotations. 2024.
DOI: 10.1007/978-3-031-72044-4_3
Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution). 2024.
DOI: 10.1007/978-3-031-57259-3_20
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).
Viktor Malík