Tools for Formal Methods: Tools

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.

CPALockator

Project URL: https://cpachecker.sosy-lab.org
Repository URL: https://gitlab.com/sosy-lab/software/cpachecker
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
Releases:
- svcomp21
Competition Participations:

CProver-witness2test

Project URL: https://www.cprover.org/cbmc/
Repository URL: https://github.com/diffblue/cbmc
Maintainers:
- Michael Tautschnig
Supported input languages:
- C
License: BSD-4-Clause
Supported techniques:
- Bounded Model Checking
Used actors / components:
- Witness Transformer: Transforms a witness to a test case.
Releases:
- svcomp23
Competition Participations:

CPV

Project URL: https://gitlab.com/sosy-lab/software/cpv
Maintainers:
- Po-Chun Chien
- Nian-Ze Lee
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
- MiniSAT
Used actors / components:
- Witness Transformer: Transforms a Btor2 hardware witness to an automata-based software witness.
- Instrumentor: Instruments a program to facilitate witness transformation.
Releases:
- 0.6
- 0.5.1
- 0.4
Literature:
- CPV: A Circuit-Based Program Verifier (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_22
Presentations:
- cpv_svcomp2024.pdf
Posters:
- cpv_svcomp2024.pdf
Competition Participations:
- SV-COMP 2025 (Verification)
- SV-COMP 2024 (Verification)

Crux

Project URL: https://crux.galois.com/
Repository URL: https://github.com/GaloisInc/crucible
Supported input languages:
- C
License: BSD-3-Clause
Supported techniques:
- Symbolic Execution
Used frameworks / solvers:
- Z3
Releases:
- svcomp23
Competition Participations:

CSeq

Project URL: https://www.southampton.ac.uk/~gp1y10/cseq/cseq.html
Maintainers:
- Emerson Sales
Supported input languages:
- C
License: BSD-4-Clause
Supported techniques:
Used frameworks / solvers:
- CProver
- MiniSAT
Used actors / components:
- Specification Transformer: Transforms from concurrent programs to sequential programs by limiting context switches.
Releases:
- svcomp22
Literature:
- Bounded Verification of Multi-threaded Programs via Lazy Sequentialization. 2022. DOI: 10.1145/3478536
- A Prototype for Data Race Detection in CSeq 3 (Competition Contribution). 2022. DOI: 10.1007/978-3-030-99527-0_23
Competition Participations:

Dartagnan

Project URL: https://github.com/hernanponcedeleon/Dat3M
Maintainers:
- Hernán Ponce de León
Supported input languages:
- C
License: MIT
Supported techniques:
Used frameworks / solvers:
- JavaSMT
Releases:
Literature:
Competition Participations:

Deagle

Project URL: https://github.com/thufv/Deagle
Maintainers:
Supported input languages:
- C
License: GPL-3.0-or-later
Supported techniques:
- Bounded Model Checking
- Concurrency Support
Used frameworks / solvers:
- MiniSAT
Releases:
Literature:
- Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution). 2022. DOI: 10.1007/978-3-030-99527-0_25
Competition Participations:

DIVINE

Project URL: https://divine.fi.muni.cz/
Repository URL: http://divine.fi.muni.cz/current
Supported input languages:
- C
License: ISC
Supported techniques:
Releases:
- svcomp22
Competition Participations:

EBF

Project URL: https://github.com/fatimahkj/EBF
Maintainers:
- Fatimah Aljaafari
Supported input languages:
- C
License: MIT
Supported techniques:
- Bounded Model Checking
Used frameworks / solvers:
- ESBMC
- MathSAT
Releases:
- svcomp24
- svcomp23
Presentations:
- ebf_svcomp2023.pdf
Competition Participations:

EmergenTheta

Project URL: https://github.com/ftsrg/theta
Maintainers:
- Levente Bajczi
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Releases:
- svcomp25
- svcomp24
Literature:
- EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_23
Presentations:
- emergentheta_svcomp2024.pdf
Competition Participations:
- SV-COMP 2025 (Verification)
- SV-COMP 2024 (Verification)

ESBMC-incr

Project URL: http://esbmc.org/
Repository URL: https://github.com/esbmc/esbmc
Maintainers:
- Lucas C. Cordeiro
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
- ESBMC
- MathSAT
Releases:
Literature:
- Verifying Multi-threaded Software Using SMT-Based Context-Bounded Model Checking. 2011. DOI: 10.1145/1985793.1985839
- Context-Bounded Model Checking with ESBMC 1.17 (Competition Contribution). 2012. DOI: 10.1007/978-3-642-28756-5_42
Competition Participations:

ESBMC-kind

Project URL: http://esbmc.org/
Repository URL: https://github.com/esbmc/esbmc
Maintainers:
- Rafael Sá Menezes
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
- ESBMC
- MathSAT
Releases:
- svcomp25
- svcomp24
- svcomp23
- testcomp25
- testcomp23
Literature:
- SMT-based bounded model checking for embedded ANSI-C software. 2011. DOI: 10.1109/TSE.2011.59
Competition Participations:

FDSE

Project URL: https://github.com/zbchen/fdse-test-comp
Maintainers:
- Zhenbang Chen
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Releases:
- testcomp25
- testcomp24
Literature:
- FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57259-3_16
Competition Participations:
- Test-Comp 2025 (Test Generation)
- Test-Comp 2024 (Test Generation)

Fizzer

Project URL: https://github.com/staticafi/sbt-fizzer
Maintainers:
- Marek Trtík
Supported input languages:
- C
License: Zlib
Supported techniques:
- Bit-Precise Analysis
Releases:
- testcomp25
- testcomp24
Literature:
- Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. 2024. DOI: 10.1007/978-3-031-57256-2_5
- Fizzer: New Gray-Box Fuzzer (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57259-3_17
Presentations:
- fizzer_testcomp2024.pdf
Competition Participations:
- Test-Comp 2025 (Test Generation)
- Test-Comp 2024 (Test Generation)

Frama-C-SV

Project URL: https://gitlab.com/sosy-lab/software/frama-c-sv
Maintainers:
- Martin Spiessl
Supported input languages:
- C
License: Apache-2.0 AND LGPL-2.0
Supported techniques:
- Numeric Interval Analysis
Releases:
- svcomp24
- svcomp23
Competition Participations:

FuSeBMC

Project URL: https://fusebmc.com/
Repository URL: https://github.com/FuSeBMC/
Maintainers:
- Kaled Alshmrany
Supported input languages:
- C
License: MIT
Supported techniques:
Releases:
Literature:
- FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis. 2024. DOI: 10.1145/3665337
Competition Participations:

FuSeBMC-AI

Project URL: https://github.com/Mohannad-Aldughaim/FuSeBMC_IA
Maintainers:
- Mohannad Aldughaim
- Kaled Alshmrany
Supported input languages:
- C
License: MIT
Supported techniques:
Releases:
- testcomp24
- testcomp23
Presentations:
- fusebmc-ia_testcomp2023.pdf
Competition Participations:

Gazer-Theta

Project URL: https://github.com/ftsrg/gazer
Maintainers:
- Zsófia Ádám
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Releases:
- svcomp23
Literature:
- Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution). 2021. DOI: 10.1007/978-3-030-72013-1_27
Competition Participations:

GDart

Project URL: https://github.com/tudo-aqua/gdart-svcomp
Maintainers:
- Falk Howar
- Malte Mues
Supported input languages:
- Java
License: Apache-2.0 AND LGPL-2.0-only
Supported techniques:
Used frameworks / solvers:
- CVC
- Z3
Releases:
Literature:
- 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
- The integration of multi-color taint-analysis with dynamic symbolic execution for Java web application security analysis. 2023. DOI: 10.17877/DE290R-23694
Competition Participations:

GDart-LLVM

Project URL: https://github.com/tudo-aqua/gdart-llvm
Maintainers:
- Falk Howar
Supported input languages:
- C
License: LGPL-2.0-only
Supported techniques:
- Bit-Precise Analysis
- Symbolic Execution
Used frameworks / solvers:
- Z3
Releases:
- svcomp23
Presentations:
- gdart-llvm_svcomp2023.pdf
Competition Participations:

Goblint

Project URL: https://goblint.in.tum.de/
Repository URL: https://github.com/goblint/analyzer
Maintainers:
- Simmo Saan
- Michael Schwarz
Supported input languages:
- C
License: MIT
Supported techniques:
Used frameworks / solvers:
- Apron
Releases:
Literature:
Presentations:
- goblint_svcomp2024.pdf
- goblint_svcomp2023.pdf
Competition Participations:

Graves-CPA

Project URL: https://github.com/will-leeson/cpachecker
Maintainers:
- Will Leeson
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
Releases:
- svcomp23
Literature:
- Graves-CPA: A Graph-Attention Verifier Selector (Competition Contribution). 2022. DOI: 10.1007/978-3-030-99527-0_28
- Algorithm Selection for Software Verification using Graph Neural Networks. 2022. DOI: 10.48550/arXiv.2201.11711
Competition Participations:

Graves-Par

Project URL: https://github.com/mgerrard/graves-par
Supported input languages:
- C
License: Apache-2.0
Releases:
- svcomp23
Competition Participations:
- SV-COMP 2024 (Verification)
- SV-COMP 2023 (Verification)

GWIT

Project URL: https://github.com/tudo-aqua/gwit
Maintainers:
- Falk Howar
Supported input languages:
- Java
License: LicenseRef-LICENSE
Supported techniques:
Releases:
- svcomp24
- svcomp23
Competition Participations:

Hornix

Project URL: https://github.com/d3sformal/hornix
Maintainers:
Supported input languages:
- C
License: Apache 2.0
Supported techniques:
- Property-Directed Reachability
Used frameworks / solvers:
- Z3
Releases:
- svcomp25
Competition Participations:
- SV-COMP 2025 (Verification)

HybridTiger

Project URL: https://www.es.tu-darmstadt.de/es/team/sebastian-ruland/testcomp20
Repository URL: https://gitlab.com/sosy-lab/software/cpachecker
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Releases:
- testcomp23
Literature:
- HybridTiger: Hybrid Model Checking and Domination-based Partitioning for Efficient Multi-Goal Test-Suite Generation (Competition Contribution). 2020. DOI: 10.1007/978-3-030-45234-6_26
Competition Participations:

Infer

Project URL: https://fbinfer.com/
Repository URL: https://gitlab.com/sosy-lab/software/infer-sv
Maintainers:
- Matthias Kettl
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used actors / components:
- Translator: Translates from Java, C, C++ to SIL for verification.
Releases:
- svcomp24
- svcomp23
Competition Participations:

Java-Ranger

Project URL: https://github.com/vaibhavbsharma/java-ranger
Maintainers:
- Soha Hussein
Supported input languages:
- Java
License: Apache-2.0
Supported techniques:
- Bit-Precise Analysis
- Symbolic Execution
Used frameworks / solvers:
- JPF
Releases:
- svcomp25
- svcomp23
Literature:
- Java Ranger at SV-COMP 2020 (Competition Contribution). 2020. DOI: 10.1007/978-3-030-45237-7_27
- Java Ranger: statically summarizing regions for efficient symbolic execution of Java. 2020. DOI: 10.1145/3368089.3409734
Competition Participations:

JayHorn

Project URL: https://github.com/jayhorn/jayhorn
Maintainers:
- Hassan Mousavi
Supported input languages:
- Java
License: LGPL-2.1-only
Supported techniques:
Releases:
- svcomp24
- svcomp23
Competition Participations:

JBMC

Project URL: https://github.com/diffblue/cbmc
Maintainers:
- Peter Schrammel
Supported input languages:
- Java
License: BSD-4-Clause
Supported techniques:
Used frameworks / solvers:
- CProver
- MiniSAT
Releases:
Literature:
- 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
Presentations:
- jbmc_svcomp2023.pdf
Competition Participations:

JCWIT

Project URL: https://github.com/Chriszai/JCWIT
Maintainers:
- Zaiyu Cheng
Supported input languages:
- Java
License: Apache-2.0
Supported techniques:
- Bounded Model Checking
Releases:
- svcomp24
Competition Participations:
- SV-COMP 2025 (Validation of Correctness Witnesses 1.0)
- SV-COMP 2024 (Validation of Correctness Witnesses 1.0)

JDart

Project URL: https://github.com/tudo-aqua/jdart
Maintainers:
- Malte Mues
Supported input languages:
- Java
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
- CVC
- JPF
- Z3
Releases:
- svcomp23
Competition Participations:

KeY

KeY is a tool for deductive verification to prove the correctness of Java programs.

Project URL: https://www.key-project.org/
Repository URL: https://github.com/KeYProject/key
Maintainers:
Supported input languages:
- Java
License: GPL-2.0
Releases:
- 2.13
Literature:

KLEE

Project URL: https://klee.github.io
Repository URL: https://github.com/klee/klee
Supported input languages:
- C
License: NCSA
Supported techniques:
Releases:
- testcomp23
Literature:
- KLEE Symbolic Execution Engine in 2019. 2020. DOI: 10.1007/s10009-020-00570-3
Competition Participations:

KLEEF

Project URL: https://toolchain-labs.com/projects/kleef.html
Repository URL: https://github.com/UnitTestBot/klee
Maintainers:
- Aleksandr Misonizhnik
Supported input languages:
- C
License: NCSA
Supported techniques:
Releases:
- testcomp25
- testcomp24
Literature:
- KLEEF: Symbolic Execution Engine (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57259-3_18
Competition Participations:
- Test-Comp 2025 (Test Generation)
- Test-Comp 2024 (Test Generation)

Korn

Project URL: https://github.com/gernst/korn
Maintainers:
- Gidon Ernst
Supported input languages:
- C
License: MIT
Supported techniques:
Used frameworks / solvers:
- Z3
Releases:
Presentations:
- korn_svcomp2024.pdf
- korn_svcomp2023.pdf
Competition Participations:

Lazy-CSeq

Project URL: https://github.com/omainv/cseq/releases
Repository URL: https://github.com/omainv/cseq
Maintainers:
- Omar Inverso
Supported input languages:
- C
License: BSD-3-Clause
Supported techniques:
Used frameworks / solvers:
- CProver
- MiniSAT
Releases:
- svcomp23
Competition Participations:

Legion

Project URL: https://github.com/Alan32Liu/Legion/tree/TestComp2020-ASE2020v3
Supported input languages:
- C
License: MIT
Supported techniques:
Releases:
- testcomp23
Competition Participations:

Legion/SymCC

Project URL: https://github.com/gernst/legion-symcc
Maintainers:
- Gidon Ernst
Supported input languages:
- C
License: MIT
Supported techniques:
Releases:
- testcomp23
Competition Participations:

LF-checker

Project URL: https://github.com/Anthonysdu/lf-checker
Maintainers:
- Tong Wu
Supported input languages:
- C
License: Apache-2.0
Releases:
- svcomp23
Presentations:
- lf-checker_svcomp2023.pdf
Competition Participations:

LIV

Project URL: https://gitlab.com/sosy-lab/software/liv
Maintainers:
- Marian Lingsch-Rosenfeld
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
- Task Translation
Used actors / components:
- Splitter: Splits a program into straight-line programs for witness validation.
- Annotator: Annotates assumes and assertions into straight-line programs for witness validation.
Releases:
- svcomp25
- svcomp24
Presentations:
- liv_svcomp2024.pdf
Competition Participations:

Locksmith

Project URL: http://www.cs.umd.edu/projects/PL/locksmith/
Repository URL: http://www.cs.umd.edu/projects/PL/locksmith/download.html
Maintainers:
- Vesal Vojdani
Supported input languages:
- C
License: BSD-3-Clause
Supported techniques:
- Concurrency Support
Releases:
- svcomp23
Competition Participations:

MetaVal

Project URL: https://gitlab.com/sosy-lab/software/metaval
Maintainers:
- Marian Lingsch-Rosenfeld
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
- Algorithm Selection
- Task Translation
Used actors / components:
- Annotator: Annotates invariants or state guards from software witnesses in the program as assertions or assumptions.
Releases:
Literature:
- MetaVal: Witness Validation via Verification. 2020. DOI: 10.1007/978-3-030-53291-8_10
Competition Participations:

MetaVal++

Project URL: https://gitlab.com/sosy-lab/software/metavalpp
Maintainers:
- Marian Lingsch-Rosenfeld
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
- Task Translation
Used actors / components:
- Annotator: Annotates invariants or state guards from software witnesses in the program as assertions or assumptions.
Releases:
- svcomp25-correctness
Competition Participations:
- SV-COMP 2025 (Validation of Correctness Witnesses 2.0)

MLB

Project URL: https://github.com/MLB-SE/Experiment
Maintainers:
- Lei Bu
Supported input languages:
- Java
License: MIT
Supported techniques:
Releases:
Literature:
- Machine learning steered symbolic execution framework for complex software code. 2021. DOI: 10.1007/s00165-021-00538-3
Competition Participations:

Mopsa

Project URL: https://gitlab.com/mopsa/mopsa-analyzer
Maintainers:
- Raphaël Monat
Supported input languages:
- C
License: LGPL-3.0-or-later
Supported techniques:
- Numeric Interval Analysis
Used frameworks / solvers:
- Apron
Releases:
Literature:
Presentations:
- mopsa_svcomp2024.pdf
- mopsa_svcomp2023.pdf
Competition Participations:

Nacpa

Project URL: https://gitlab.com/sosy-lab/software/nacpa
Maintainers:
- Thomas Lemberger
- Henrik Wachowitz
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
- Algorithm Selection
- Portfolio
Used frameworks / solvers:
- CPAchecker
Releases:
- 1.0.0
Competition Participations:
- SV-COMP 2025 (Verification)

NITWIT

Project URL: https://github.com/moves-rwth/nitwit-validator/
Maintainers:
- Jana (Philipp) Berger
Supported input languages:
- C
License: BSD-3-Clause
Supported techniques:
- Explicit-Value Analysis
Releases:
- svcomp24-validation-violation
- svcomp23-validation-violation
Literature:
- Interpretation-Based Violation Witness Validation for C: NITWIT. 2020. DOI: 10.1007/978-3-030-45190-5_3
Competition Participations:

Owi

Project URL: https://ocamlpro.github.io/owi
Repository URL: https://github.com/OCamlPro/owi
Maintainers:
- Léo Andrès
- Filipe Marques
Supported input languages:
- C
- Wasm
License: AGPL-3.0-only
Supported techniques:
Releases:
- testcomp24
Competition Participations:
- Test-Comp 2025 (Test Generation)
- Test-Comp 2024 (Test Generation)

PeSCo-CPA

Project URL: https://github.com/cedricrupb/pesco
Maintainers:
- Cedric Richter
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
Releases:
- svcomp24
- svcomp23
Competition Participations:

PIChecker

Project URL: https://gitlab.com/Lapulatos/pichecker
Maintainers:
- Jie Su
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
Releases:
- svcomp23
Competition Participations:

Pinaka

Project URL: https://github.com/sbjoshi/Pinaka
Maintainers:
- Saurabh Joshi
Supported input languages:
- C
License: BSD-4-Clause
Supported techniques:
Releases:
- svcomp23
Literature:
- Pinaka: Symbolic Execution Meets Incremental Solving (Competition Contribution). 2019. DOI: 10.1007/978-3-030-17502-3_20
Competition Participations:

PredatorHP

Project URL: https://www.fit.vutbr.cz/research/groups/verifit/tools/predatorhp/
Repository URL: https://github.com/versokova/predatorhp
Maintainers:
- Veronika Šoková
Supported input languages:
- C
License: GPL-3.0-or-later
Supported techniques:
- Shape Analysis
Releases:
- svcomp24
- svcomp23
Literature:
Presentations:
- predatorhp_svcomp2024.pdf
Competition Participations:

PROTON

Project URL: https://github.com/kumarmadhukar/term
Maintainers:
- Ravindra Metta
Supported input languages:
- C
License: MIT
Supported techniques:
- Bounded Model Checking
Releases:
- svcomp25
- svcomp24
Literature:
- Proton: Probes for Non-termination and Termination (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_27
Presentations:
- proton_svcomp2024.pdf
Competition Participations:
- SV-COMP 2025 (Verification)
- SV-COMP 2024 (Verification)

PRTest

Project URL: https://gitlab.com/sosy-lab/software/prtest
Maintainers:
- Thomas Lemberger
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
- Floating-Point Arithmetics
- Random Execution
Releases:
- testcomp24
- testcomp23
Literature:
- Plain random test generation with PRTest. 2021. DOI: 10.1007/s10009-020-00568-x
Competition Participations:

RacerF

Project URL: https://github.com/TDacik/Deadlock_Racer
Maintainers:
- Tomáš Dacík
- Tomáš Vojnar
Supported input languages:
- C
License: MIT
Supported techniques:
- Concurrency Support
Releases:
- svcomp25
Competition Participations:
- SV-COMP 2025 (Verification)

RELAY-SV

Project URL: https://cseweb.ucsd.edu/~jvoung/race
Repository URL: https://github.com/vesalvojdani/relay-sv
Maintainers:
- Vesal Vojdani
Supported input languages:
- C
License: BSD-3-Clause
Supported techniques:
- Concurrency Support
- Symbolic Execution
Releases:
- svcomp24
Literature:
- RELAY: static race detection on millions of lines of code. 2007. DOI: 10.1145/1287624.1287654
Competition Participations:
- SV-COMP 2024 (Verification)

Rizzer

Project URL: https://github.com/staticafi/sbt-fizzer/tree/rizzer
Maintainers:
- Adam Štafa
Supported input languages:
- C
License: Zlib
Supported techniques:
- Bit-Precise Analysis
- Symbolic Execution
Releases:
- testcomp24
Competition Participations:
- Test-Comp 2025 (Test Generation)
- Test-Comp 2024 (Test Generation)

Sikraken

Project URL: https://github.com/echancrure/Sikraken
Maintainers:
- Christophe Meudec
Supported input languages:
- C
License: LGPL-3.0-only
Supported techniques:
- Symbolic Execution
Releases:
- 1.0.8
Competition Participations:
- Test-Comp 2025 (Test Generation)

SPF

Project URL: https://github.com/SymbolicPathFinder/jpf-symbc
Maintainers:
- Yannic Noller
Supported input languages:
- Java
License: Apache-2.0
Supported techniques:
Used frameworks / solvers:
- JPF
Releases:
- svcomp23
Literature:
- Combining Unit-Level Symbolic Execution and System-Level Concrete Execution for Testing NASA Software. 2008. DOI: 10.1145/1390630.1390635
Competition Participations:

sv-sanitizers

Project URL: https://github.com/sim642/sv-sanitizers
Maintainers:
- Simmo Saan
Supported input languages:
- C
License: MIT
Supported techniques:
- Concurrency Support
- Random Execution
Releases:
- svcomp25
- svcomp24
Competition Participations:
- SV-COMP 2025 (Verification)
- SV-COMP 2024 (Verification)

SVF-SVC

Project URL: https://github.com/Lasagnenator/svf-svc-comp/
Maintainers:
- Matthew Richards
- Cameron McGowan
Supported input languages:
- C
License: AGPL-3.0-or-later
Releases:
- svcomp25
Competition Participations:
- SV-COMP 2025 (Verification)

SWAT

Project URL: https://www.its.uni-luebeck.de/en/research/tools/swat/
Repository URL: https://github.com/SWAT-project/SWAT
Maintainers:
- Nils Loose
- Felix Maechtle
Supported input languages:
- Java
License: BSD-2-Clause
Supported techniques:
- Symbolic Execution
Used frameworks / solvers:
- Z3
Releases:
- svcomp24
- svcomp25
Literature:
- SWAT: Modular Dynamic Symbolic Execution for Java Applications Using Dynamic Instrumentation (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_28
Presentations:
- swat_svcomp2024.pdf
Competition Participations:
- SV-COMP 2025 (Verification)
- SV-COMP 2024 (Verification)

Symbiotic

Project URL: https://github.com/staticafi/symbiotic
Maintainers:
- Martin Jonáš
Supported input languages:
- C
License: MIT
Supported techniques:
Used frameworks / solvers:
- Z3
Used actors / components:
- Slicer: Slices the program before symbolic execution.
- Instrumentor: Instruments the program to track allocated memory regions for memory-safety analysis.
Releases:
- svcomp25
- testcomp25
- svcomp24
- testcomp24
- svcomp23
- testcomp23
Literature:
Presentations:
- symbiotic_svcomp2024.pdf
Competition Participations:

Symbiotic-Witch

Project URL: https://github.com/ayazip/witch-klee
Maintainers:
- Paulína Ayaziová
Supported input languages:
- C
License: MIT
Supported techniques:
- Symbolic Execution
Releases:
Literature:
- Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution). 2023. DOI: 10.1007/978-3-031-30820-8_30
- Symbiotic-Witch: A Klee-Based Violation Witness Checker (Competition Contribution). 2022. DOI: 10.1007/978-3-030-99527-0_33
Presentations:
- symbiotic-witch_svcomp2023.pdf
Competition Participations:

TestCov

Project URL: https://gitlab.com/sosy-lab/software/test-suite-validator
Maintainers:
- Matthias Kettl
- Thomas Lemberger
Supported input languages:
- C
License: Apache-2.0
Releases:
Literature:
- TestCov: Robust Test-Suite Execution and Coverage Measurement. 2019. DOI: 10.1109/ASE.2019.00105
Competition Participations:

Theta

Project URL: https://github.com/ftsrg/theta
Maintainers:
- Levente Bajczi
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Releases:
Literature:
- Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_30
Presentations:
- theta_svcomp2024.pdf
Competition Participations:

Thorn

Project URL: https://github.com/ftsrg/theta
Maintainers:
- Levente Bajczi
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Releases:
- svcomp25
Competition Participations:
- SV-COMP 2025 (Verification)

TracerX

Project URL: https://tracer-x.github.io/
Repository URL: https://github.com/tracer-x/TracerX
Maintainers:
- Joxan Jaffar
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
Releases:
Literature:
- TracerX: Dynamic Symbolic Execution with Interpolation (Competition Contribution). 2020. DOI: 10.1007/978-3-030-45234-6_28
Competition Participations:

TracerX-WP

Project URL: https://tracer-x.github.io/
Repository URL: https://github.com/tracer-x/TracerX
Maintainers:
- Joxan Jaffar
Supported input languages:
- C
License: Apache-2.0
Supported techniques:
- Interpolation
Releases:
- testcomp25
- testcomp24
Literature:
- TracerX: Pruning Dynamic Symbolic Execution with Deletion and Weakest Precondition Interpolation (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57259-3_19
Competition Participations:
- Test-Comp 2025 (Test Generation)
- Test-Comp 2024 (Test Generation)

UAutomizer

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.