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
AFL-to-Test-Case is a tool that uses AFL to produce test cases.
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
BRICK is a bounded reachability checker for embedded C programs. BRICK conducts a path-oriented style checking of the bounded state space of the program, that enumerates and checks all the possible paths of the program in the threshold one by one. BRICK locates and records unsatisfiable core path segments to prune the search space to alleviate the path explosion problem.
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. Currently, CW2T does not use any sophisticated pre-transformation steps to manage incomplete witnesses, and it also does not support the full witness specification. For example, assumptions that aren't interpretable as single-value assignments of a nondeterministic funcion are ignored.
CoOpeRace is a no-data-race meta-verifier with the goal to combine and cross-validate detailed race warnings on real-world programs. On SV-COMP we identify the highest-scoring portfolio of current verifiers.
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
CPV is a software verifier for C programs that uses sequential circuits as its intermediate representation and leverages hardware model checkers to perform reachability and termination analysis.
CSeq is a static analysis tool for multi-threaded C programs. It is based on sequentialisation, where the program under analysis is converted into an equivalent (up to a given context bound) sequential program. For the competition, CSeq relies on CBMC for the actual analysis of the sequential program.
Dartagnan is a bounded model checking tool for weak memory concurrency.
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
DASA (Differentiable Abstract Symbolic Analyzer) is an optimization-driven engine for symbolic program analysis. Instead of controlling execution paths with traditional constraint solvers, DASA exports the System under Test (SuT) as a function graph: each node corresponds to a function that is modeled as a compact mathematical mapping. On this representation, DASA applies ML-like optimization techniques to discover inputs that lead to new paths, states, or target conditions.
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.
ESBMC (the Efficient SMT-based Context-Bounded Model Checker) is a mature, permissively licensed open-source context-bounded model checker that automatically detects or proves the absence of runtime errors in single- and multi-threaded C, C++, CUDA, CHERI, Kotlin, Python, and Solidity programs. It can automatically verify predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions.
ESBMC (the Efficient SMT-based Context-Bounded Model Checker) is a mature, permissively licensed open-source context-bounded model checker that automatically detects or proves the absence of runtime errors in single- and multi-threaded C, C++, CUDA, CHERI, Kotlin, Python, and Solidity programs. It can automatically verify predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions.
Fizzer is a gray-box fuzzer focussing of coverage of atomic Boolean expressions (mainly number comparison instructions). It uses dynamic taint-flow analysis and local space fuzzing (gradient descent, bit and random mutations performed in local spaces).
FuncTion-Res is a research prototype static analyzer designed for proving conditional termination, conditional termination resilience and conditional CTL properties of C programs. It is also capable of inferring minimal sets of variables with an associate sufficient precondition to ensure a CTL property and maximal sets of variables for which a valuation might falsify it. The tool automatically infers piecewise-defined ranking functions and sufficient preconditions by means of abstract interpretation.
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 implements dynamic symbolic execution by obtaining traces from concolic runs in the SPouT component and joining them into a symbolic constraint tree in the DSE component. In the backend of the DSE component, we use SMT solvers to identify candidate values for seeding concrete runs. This seeding allows to explore different branches following the ideas presented in the context of the `DART: directed automated random testing` paper by Godefroid et al. presented in 2005 (https://doi.org/10.1145/1064978.1065036). Today, GDart is implemented as an ensemble of different tools. The core of SPouT extends the Espresso VM part of the GraalVM project and is licensed under GPL-2.0. The GraalVM itself is licensed under LGPL-2.0. The DSE and verifier_stub components are licensed under Apache-2.0. There are more components involved, however, we leave the clarificaiton of further licensing explanations to the LICENSE file in the gdart-tool folder.
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
Goblint-Par is a parallel variant of Goblint.
Goblitch combines Goblint's abstract interpretation with the Witch validator. It iteratively refines Goblint's precision by generating candidate error paths and using symbolic execution to confirm or refute the paths until a feasible counterexample is found or the search is exhausted.
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 Golem to decide about its satisfiability.
Iekke is an partial-order-based bounded model checker for concurrent program verification. It is built on top of Deagle (front-end) and MiniSAT-2.2.1 (back-end). Iekke uses the general Deagle infrastructure, but replacing the modules responsible for creating concurrency constraints (via partial order) with new modules that produce constraints inspired by Lazy-CSeq sequentializzation. This allows for a smaller formula size for analyzing concurrent programs compared to the classic partial order. These new modules can also be imported into CBMC, as it shares the same infrastructure as Deagle. Furthermore, the Deagle solver has been replaced with MiniSAT.
JayHorn is a software model checking tool for Java that attempts to prove certain bad states in a program are never reachable and aims to be sound.
JayHorn: A Framework for Verifying Java programs. 2016.
DOI: 10.1007/978-3-319-41540-6_14
JayHorn: A Java Model Checker. 2019.
DOI: 10.1145/3340672.3341113
JayHorn: A Java Model Checker: (Competition Contribution). 2019.
DOI: 10.1007/978-3-030-17502-3_16
Towards string support in JayHorn (competition contribution). 2021.
DOI: 10.1007/978-3-030-72013-1_29
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
JLisa is the java frontend of LiSA, a Java library that provides a complete infrastructure for the development of static analyzers based on abstract interpretation. In particular, LiSA implements several standard components of abstract interpretation-based analyzers, such as an extensible control-flow graph representation (CFG), a common analysis framework for the development of new static analyses, and fixpoint algorithms on LiSA CFGs. JLiSA implements custom abstract domains such as constant propagation and intervals to verify the correctness of Java programs. In particular, it verifies that assertions never fail and that no uncaught runtime exceptions exist.
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.
LTSmin is a language-independent model-checking toolset supporting multiple input languages and advanced state-space generation techniques via a unified PINS interface. It features modular architecture, symbolic/distributed/multi-core reachability, and easy extensibility for new languages.
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.
MLB is a symbolic execution tool with a machine learning approach for constraint solving. MLB supports the symbolic execution of not only simple linear path conditions, but also nonlinear arithmetic operations, and even black-box function calls of library methods. Meanwhile, thanks to the theoretical foundation of the machine learning based approach, when the solver fails to solve a path condition, we can have an estimation of the confidence in the satisfiability (ECS) of the problem to give users insights about how the problem is analyzed and whether they could ultimately find a solution.
MOPSA - A Modular Open Platform for Static Analysis is a research-oriented platform written in OCaml to build sound semantic static analyzers based on Abstract Interpretation. Our goal with MOPSA is to encourage the research and education in Abstract Interpretation by providing a fully-featured and extensible open-source platform and usable analyses built with it. MOPSA supports the analysis of multiple programming languages and leverages relational numerical domains.
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
Mopsa-C with Trace Partitioning and Autosuggestions (Competition Contribution). 2025.
DOI: 10.1007/978-3-031-90660-2_17
MuVal is a validity checker for fixpoint logics modulo background theories.
Nacpa is a meta-verifier for C programs. It utilizes CPAchecker as a backend verifier and Kleef and PRTest for dynamic reach safety analysis. It is based on strategy selection, parallel portfolios, and native compilation of Java.
OGChecker is built on top of CPAchecker4.1 and utilizes the observing graph-based partial-order technique for efficient verification of concurrent programs.
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
PROTON is a tool to check whether a given C program has a non-terminating behaviour or not. It is built around the C Bounded Model Checker (CBMC). PROTON first annotates the loops in a given program with assertions that check for a recurrent program state. Violation of such an assertion shows the existence of a recurrent state and thereby proves non-termination. If PROTON is unable to find non-termination within a few minutes, it then performs an unsound termination check based on checking CBMC's unwinding assertions.
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.
Re3ver is a tool for reachability analysis, integrating a preprocessor which reverses the input programs into the verifier Symbiotic.
SEAL is a static analyzer aimed at verifying programs that work with dynamic memory, especially linked lists. It is implemented as a plugin for the Frama-C framework. The analysis is based on abstract interpretation with a domain of separation logic formulae representing abstract memory states. For deciding SL formulae, SEAL uses Astral, a dedicated solver for separation logic.
SV-COMP wrapper for sanitizers (ThreadSanitizer, AddressSanitizer, LeakSanitizer, UndefinedBehaviorSanitizer).
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.
SWAT (Symbolic Web Application Testing) is an advanced tool for analyzing Java web applications for security vulnerabilities and errors, based on concolic execution. It employs dynamic symbolic execution to precisely identify weaknesses. The modular system utilizes JavaSMT for formula creation and strategically coordinates tests with Z3 as the symbolic solver. Ideal for developers who want to test their web applications securely and efficiently.
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 Paralizer is a software model checker that is based on parallel trace abstraction. It analyis multiple counterexample in parallel, including: feasibility checks, interpolation and refinements.
Ultimate Referee is a deductive verifier. It checks whether annotated invariants are sufficient to establish an inductive proof. In particular, Referee does not try and infer invariants, it only checks them. Invariants can also be provided as correctness witnesses, which makes Referee a strict 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
The VerCors verifier is a tool for deductive verification of concurrent and parallel software. VerCors can reason about programs written in different programming languages, such as Java, C and OpenCL, where the specifications are written in terms of pre-post-condition contracts using permission-based separation logic. VerCors is able to reason about data-race freedom, memory safety, and functional correctness, and it has been applied on several realistic case studies. Several tools are being developed directly on top of VerCors by encoding their input languages to VerCors' internal representation, allowing reuse of the existing infrastructure for verification. These tools are Alpinist, Vesuv, and VeyMont.
Wit4java is a violation witness validator for java verifiers.
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