Tools for Formal Methods: Tools

2LS

• Project URL: https://github.com/diffblue/2ls
• Maintainers:
  • Viktor Malík
• Supported input languages:
  • C
• License: BSD-4-Clause
• Supported techniques:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • k-Induction
  • Numeric Interval Analysis
  • Ranking Functions
  • Shape Analysis
• Used frameworks / solvers:
  • CProver
  • MiniSAT
• Releases:
  • svcomp24
  • svcomp23
• Literature:
  • Safety Verification and Refutation by k-Invariants and k-Induction. 2015. DOI: 10.1007/978-3-662-48288-9_9
  • 2ls: Arrays and Loop Unwinding (Competition Contribution). 2023. DOI: 10.1007/978-3-031-30820-8_31
  • 2ls: Heap Analysis and Memory Safety (Competition Contribution). 2020. DOI: 10.1007/978-3-030-45237-7_22
  • 2ls for Program Analysis (Competition Contribution). 2016. DOI: 10.1007/978-3-662-49674-9_56
• Presentations:
  • 2ls_svcomp2023.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

aise

• Project URL: https://github.com/ZhenWang233/AISE
• Maintainers:
  • Zhenbang Chen
• Supported input languages:
  • C
• License: GPL-3.0-or-later
• Supported techniques:
  • Symbolic Execution
• Releases:
  • svcomp24
• Literature:
  • AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_19
• Competition Participations:
  • SV-COMP 2024 (Verification)

AProVE

• Project URL: https://aprove.informatik.rwth-aachen.de/
• Maintainers:
  • Jan-Christoph Kassing
• Supported input languages:
  • C
• License: AProVE license
• Supported techniques:
  • Ranking Functions
• Used frameworks / solvers:
  • Z3
• Releases:
  • svcomp22
• Literature:
  • AProVE: Non-Termination Witnesses for C Programs (Competition Contribution). 2022. DOI: 10.1007/978-3-030-99527-0_21
• Competition Participations:
  • SV-COMP 2022 (Verification)

BRICK

• Project URL: https://github.com/brick-tool-dev/BRICK-2.0
• Maintainers:
  • Lei Bu
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Bounded Model Checking
  • CEGAR
  • Concurrency Support
  • Numeric Interval Analysis
  • Symbolic Execution
• Used frameworks / solvers:
  • MiniSAT
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Literature:
  • Brick: Path Enumeration-Based Bounded Reachability Checking of C Programs (Competition Contribution). 2022. DOI: 10.1007/978-3-030-99527-0_22
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

Bubaak

• Project URL: https://gitlab.com/mchalupa/bubaak
• Maintainers:
  • Marek Chalupa
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Bit-Precise Analysis
  • Concurrency Support
  • Portfolio
  • Ranking Functions
  • Symbolic Execution
• Used frameworks / solvers:
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Literature:
  • Bubaak: Runtime Monitoring of Program Verifiers (Competition Contribution). 2023. DOI: 10.1007/978-3-031-30820-8_32
• Presentations:
  • bubaak_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

Bubaak-SpLit

• Project URL: https://gitlab.com/mchalupa/bubaak
• Maintainers:
  • Marek Chalupa
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Algorithm Selection
  • Automata-Based Analysis
  • Bit-Precise Analysis
  • Concurrency Support
  • k-Induction
  • Portfolio
  • Ranking Functions
  • Symbolic Execution
• Used actors / components:
  • Splitter: Splits a program and verifies in parallel.
• Releases:
  • svcomp24
• Literature:
  • Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_20
• Presentations:
  • bubaak-split_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)

CBMC

• 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:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Concurrency Support
• Used frameworks / solvers:
  • CProver
  • MiniSAT
• Used actors / components:
  • Translator: Translates from C to a Goto program for verification.
• Releases:
  • svcomp23
• Literature:
  • CBMC: C Bounded Model Checker (Competition Contribution). 2014. DOI: 10.1007/978-3-642-54862-8_26
  • A Tool for Checking ANSI-C Programs. 2004. DOI: 10.1007/978-3-540-24730-2_15
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

cetfuzz

• Project URL: https://gitlab.com/Sarathkrishnan/cetfuzz
• Maintainers:
  • Sarath Krishnan G S
  • Seth Shaji George
  • Raveendra Kumar Medicherla
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • Evolutionary Algorithms
• Releases:
  • testcomp24
• Competition Participations:
  • Test-Comp 2024 (Test Generation)

COASTAL

• Project URL: https://www.cs.sun.ac.za/coastal
• Repository URL: https://github.com/DeepseaPlatform/coastal
• Maintainers:
  • Willem Visser
• Supported input languages:
  • Java
• License: Apache-2.0
• Supported techniques:
  • Symbolic Execution
• Used frameworks / solvers:
  • JPF
• Releases:
  • svcomp20
• Literature:
  • Coastal: Combining Concolic and Fuzzing for Java (Competition Contribution). 2020. DOI: 10.1007/978-3-030-45237-7_23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

ConcurrentWitness2Test

• Project URL: https://github.com/ftsrg/ConcurrentWitness2Test
• Maintainers:
  • Levente Bajczi
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Concurrency Support
• Releases:
  • svcomp24
• Literature:
  • ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_16
• Presentations:
  • concurrentwitness2test_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)

CoVeriTeam-Verifier-AlgoSelection

• Project URL: https://gitlab.com/sosy-lab/software/coveriteam
• Maintainers:
  • Henrik Wachowitz
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • ARG-Based Analysis
  • Automata-Based Analysis
  • Bit-Precise Analysis
  • Bounded Model Checking
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • k-Induction
  • Lazy Abstraction
  • Numeric Interval Analysis
  • Portfolio
  • Predicate Abstraction
  • Ranking Functions
  • Shape Analysis
  • Symbolic Execution
• Used frameworks / solvers:
  • CPAchecker
  • CProver
  • ESBMC
  • JavaSMT
  • MathSAT
  • MiniSAT
  • Ultimate
• Releases:
  • svcomp23
• Literature:
  • Construction of Verifier Combinations Based on Off-the-shelf Verifiers. 2022. DOI: 10.1007/978-3-030-99429-7_3
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

CoVeriTeam-Verifier-ParallelPortfolio

• Project URL: https://gitlab.com/sosy-lab/software/coveriteam
• Maintainers:
  • Henrik Wachowitz
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • Bounded Model Checking
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • k-Induction
  • Lazy Abstraction
  • Numeric Interval Analysis
  • Portfolio
  • Predicate Abstraction
  • Ranking Functions
  • Shape Analysis
  • Symbolic Execution
• Used frameworks / solvers:
  • CPAchecker
  • CProver
  • ESBMC
  • JavaSMT
  • MathSAT
  • MiniSAT
  • Ultimate
• Releases:
  • svcomp23
• Literature:
  • Construction of Verifier Combinations Based on Off-the-shelf Verifiers. 2022. DOI: 10.1007/978-3-030-99429-7_3
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

CoVeriTest

• Project URL: https://cpachecker.sosy-lab.org/
• Repository URL: https://gitlab.com/sosy-lab/software/cpachecker
• Maintainers:
  • Marie-Christine Jakobs
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • CEGAR
  • Explicit-Value Analysis
  • Floating-Point Arithmetics
  • Portfolio
  • Predicate Abstraction
• Used actors / components:
  • Specification Transformer: Transforms from test goals to error locations and use reachability analyzers to generate tests.
• Releases:
  • testcomp24
  • testcomp23
• Presentations:
  • coveritest_testcomp2024.pdf
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

CPA-BAM-BnB

• 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:
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • CEGAR
  • Explicit-Value Analysis
  • Interpolation
  • Lazy Abstraction
  • Predicate Abstraction
• Used frameworks / solvers:
  • CPAchecker
  • JavaSMT
  • MathSAT
• Releases:
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

CPA-BAM-SMG

• Project URL: https://cpachecker.sosy-lab.org
• Repository URL: https://gitlab.com/sosy-lab/software/cpachecker
• Supported input languages:
  • C
• License: Apache-2.0
• Used frameworks / solvers:
  • CPAchecker
  • JavaSMT
  • MathSAT
• Releases:
  • svcomp22
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

CPA-witness2test

• Project URL: https://cpachecker.sosy-lab.org
• Repository URL: https://gitlab.com/sosy-lab/software/cpachecker
• Maintainers:
  • Dirk Beyer
  • Philipp Wendler
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • ARG-Based Analysis
  • Automata-Based Analysis
  • Property-Directed Reachability
• Used actors / components:
  • Witness Transformer: Transforms a witness to a test case.
• Releases:
  • 2.3
  • 2.2
  • svcomp22-validation-violation
• Literature:
  • Tests from Witnesses: Execution-Based Validation of Verification Results. 2018. DOI: 10.1007/978-3-319-92994-1_1
• Competition Participations:
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Validation of Violation Witnesses 1.0)

CPAchecker

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.

• Project URL: https://cpachecker.sosy-lab.org
• Repository URL: https://gitlab.com/sosy-lab/software/cpachecker
• Maintainers:
  • Dirk Beyer
  • Philipp Wendler
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • ARG-Based Analysis
  • Automata-Based Analysis
  • Bit-Precise Analysis
  • Bounded Model Checking
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • k-Induction
  • Lazy Abstraction
  • Numeric Interval Analysis
  • Portfolio
  • Predicate Abstraction
  • Property-Directed Reachability
  • Ranking Functions
  • Separation Logic
  • Shape Analysis
  • Symbolic Execution
• Used frameworks / solvers:
  • Apron
  • CPAchecker
  • JavaSMT
  • MathSAT
• Releases:
  • 2.3.1
  • 2.3
  • svcomp24-correctness
  • svcomp24-violation
  • 2.2
  • svcomp22
  • 2.1
• Literature:
  • 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
• Presentations:
  • cpachecker_svcomp2024.pdf
  • cpachecker_svcomp2023.pdf
• Posters:
  • cpachecker_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2024 (Validation of Correctness Witnesses 1.0)
  • SV-COMP 2024 (Validation of Correctness Witnesses 2.0)
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2024 (Validation of Violation Witnesses 2.0)
  • SV-COMP 2023 (Verification)

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:
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • Lazy Abstraction
  • Predicate Abstraction
• Used frameworks / solvers:
  • CPAchecker
  • JavaSMT
  • MathSAT
• Releases:
  • svcomp21
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Validation of Violation Witnesses 1.0)

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:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • CEGAR
  • Interpolation
  • k-Induction
  • Logic Synthesis
  • Portfolio
  • Predicate Abstraction
  • Property-Directed Reachability
  • Task Translation
• 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:
  • svcomp24
• 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 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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Concurrency Support
• 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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

Dartagnan

• Project URL: https://github.com/hernanponcedeleon/Dat3M
• Maintainers:
  • Hernán Ponce de León
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Concurrency Support
• Used frameworks / solvers:
  • JavaSMT
• Releases:
  • svcomp24
  • svcomp23
• Literature:
  • Portability Analysis for Weak Memory Models PORTHOS: One Tool for all Models. 2017. DOI: 10.1007/978-3-319-66706-5_15
  • BMC with Memory Models as Modules. 2018. DOI: 10.23919/FMCAD.2018.8603021
  • 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
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Verification)

Deagle

• Project URL: https://github.com/thufv/Deagle
• Maintainers:
  • Fei He
• Supported input languages:
  • C
• License: GPL-3.0-or-later
• Supported techniques:
  • Bounded Model Checking
  • Concurrency Support
• Used frameworks / solvers:
  • MiniSAT
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

DIVINE

• Project URL: https://divine.fi.muni.cz/
• Repository URL: http://divine.fi.muni.cz/current
• Supported input languages:
  • C
• License: ISC
• Supported techniques:
  • Algorithm Selection
  • Bit-Precise Analysis
  • Concurrency Support
  • Explicit-Value Analysis
  • Portfolio
  • Symbolic Execution
• Releases:
  • svcomp22
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

EmergenTheta

• Project URL: https://github.com/ftsrg/theta
• Maintainers:
  • Levente Bajczi
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Interpolation
  • k-Induction
  • Portfolio
• Releases:
  • svcomp24
• Presentations:
  • emergentheta_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)

ESBMC-incr

• Project URL: http://esbmc.org/
• Repository URL: https://github.com/esbmc/esbmc
• Maintainers:
  • Felipe R. Monteiro
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Concurrency Support
  • k-Induction
• Used frameworks / solvers:
  • ESBMC
  • MathSAT
• Releases:
  • svcomp22
• 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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Concurrency Support
  • Explicit-Value Analysis
  • Floating-Point Arithmetics
  • k-Induction
  • Numeric Interval Analysis
• Used frameworks / solvers:
  • ESBMC
  • MathSAT
• Releases:
  • svcomp24
  • svcomp23
  • testcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

FDSE

• Project URL: https://github.com/passengerZ/FDSE
• Maintainers:
  • Zhenbang Chen
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • Random Execution
  • Symbolic Execution
• Releases:
  • testcomp24
• Competition Participations:
  • 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:
  • 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 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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

FuSeBMC

• Project URL: https://github.com/kaled-alshmrany/FuSeBMC
• Maintainers:
  • Kaled Alshmrany
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Bounded Model Checking
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • Portfolio
  • Targeted Input Generation
• Releases:
  • testcomp24
  • testcomp23
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

FuSeBMC-AI

• Project URL: https://github.com/Mohannad-Aldughaim/FuSeBMC_IA
• Repository URL: https://github.com/kaled-alshmrany/FuSeBMC
• Maintainers:
  • Mohannad Aldughaim
  • Kaled Alshmrany
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Bounded Model Checking
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • Portfolio
  • Targeted Input Generation
• Releases:
  • testcomp24
  • testcomp23
• Presentations:
  • fusebmc-ia_testcomp2023.pdf
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

Gazer-Theta

• Project URL: https://github.com/ftsrg/gazer
• Maintainers:
  • Zsófia Ádám
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • Bounded Model Checking
  • CEGAR
  • Explicit-Value Analysis
  • Interpolation
  • Lazy Abstraction
  • Portfolio
  • Predicate Abstraction
• 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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

GDart

• Project URL: https://github.com/tudo-aqua/gdart-svcomp
• Maintainers:
  • Falk Howar
• Supported input languages:
  • Java
• License: Apache-2.0 AND LGPL-2.0-only
• Supported techniques:
  • Bit-Precise Analysis
  • Portfolio
  • Symbolic Execution
• Used frameworks / solvers:
  • CVC
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • Algorithm Selection
  • Concurrency Support
  • Numeric Interval Analysis
• Used frameworks / solvers:
  • Apron
• Releases:
  • svcomp24
  • svcomp24-validation-correctness
  • svcomp23
• Presentations:
  • goblint_svcomp2024.pdf
  • goblint_svcomp2023.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2024 (Validation of Correctness Witnesses 2.0)
  • SV-COMP 2023 (Verification)

Graves-CPA

• Project URL: https://github.com/will-leeson/cpachecker
• Maintainers:
  • Will Leeson
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • Bounded Model Checking
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • k-Induction
  • Lazy Abstraction
  • Numeric Interval Analysis
  • Portfolio
  • Predicate Abstraction
  • Ranking Functions
  • Shape Analysis
• Used frameworks / solvers:
  • CPAchecker
  • JavaSMT
  • MathSAT
• 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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • Bit-Precise Analysis
  • Portfolio
  • Symbolic Execution
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Validation of Violation Witnesses 1.0)

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:
  • CEGAR
  • Explicit-Value Analysis
  • Floating-Point Arithmetics
  • Predicate Abstraction
• 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:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

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:
  • Numeric Interval Analysis
  • Portfolio
  • Separation Logic
  • Shape Analysis
• Used actors / components:
  • Translator: Translates from Java, C, C++ to SIL for verification.
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

JayHorn

• Project URL: https://github.com/jayhorn/jayhorn
• Maintainers:
  • Hassan Mousavi
• Supported input languages:
  • Java
• License: LGPL-2.1-only
• Supported techniques:
  • CEGAR
  • Interpolation
  • Lazy Abstraction
  • Numeric Interval Analysis
  • Predicate Abstraction
  • Property-Directed Reachability
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

JBMC

• Project URL: https://github.com/diffblue/cbmc
• Maintainers:
  • Peter Schrammel
• Supported input languages:
  • Java
• License: BSD-4-Clause
• Supported techniques:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Concurrency Support
• Used frameworks / solvers:
  • CProver
  • MiniSAT
• Releases:
  • svcomp24
  • svcomp23
• 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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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 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:
  • Bit-Precise Analysis
  • Portfolio
  • Symbolic Execution
• Used frameworks / solvers:
  • CVC
  • JPF
  • Z3
• Releases:
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • Wolfgang Ahrendt
  • Bernhard Beckert
  • Richard Bubel
  • Reiner Hähnle
  • Mattias Ulbrich
  • Alexander Weigl
• Supported input languages:
  • Java
• License: GPL-2.0
• Releases:
  • 2.13
• Literature:
  • 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

KLEE

• Project URL: https://klee.github.io
• Repository URL: https://github.com/klee/klee
• Supported input languages:
  • C
• License: NCSA
• Supported techniques:
  • Floating-Point Arithmetics
  • Symbolic Execution
  • Targeted Input Generation
• Releases:
  • testcomp23
• Literature:
  • KLEE Symbolic Execution Engine in 2019. 2020. DOI: 10.1007/s10009-020-00570-3
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

KLEEF

• Project URL: https://toolchain-labs.com/projects/kleef.html
• Repository URL: https://github.com/UnitTestBot/klee
• Maintainers:
  • Yurii Kostyukov
• Supported input languages:
  • C
• License: NCSA
• Supported techniques:
  • Bit-Precise Analysis
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • Symbolic Execution
  • Targeted Input Generation
• Releases:
  • testcomp24
• Competition Participations:
  • Test-Comp 2024 (Test Generation)

Korn

• Project URL: https://github.com/gernst/korn
• Maintainers:
  • Gidon Ernst
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Explicit-Value Analysis
  • Portfolio
  • Predicate Abstraction
  • Symbolic Execution
• Used frameworks / solvers:
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Presentations:
  • korn_svcomp2024.pdf
  • korn_svcomp2023.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Concurrency Support
• Used frameworks / solvers:
  • CProver
  • MiniSAT
• Releases:
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

Legion

• Project URL: https://github.com/Alan32Liu/Legion/tree/TestComp2020-ASE2020v3
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Explicit-Value Analysis
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • Random Execution
  • Symbolic Execution
  • Targeted Input Generation
• Releases:
  • testcomp23
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

Legion/SymCC

• Project URL: https://github.com/gernst/legion-symcc
• Maintainers:
  • Gidon Ernst
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Explicit-Value Analysis
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • Random Execution
  • Symbolic Execution
  • Targeted Input Generation
• Releases:
  • testcomp23
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

LIV

• Project URL: https://gitlab.com/sosy-lab/software/liv
• Maintainers:
  • Martin Spiessl
• 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:
  • svcomp24
• Presentations:
  • liv_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Validation of Correctness Witnesses 1.0)

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:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

MetaVal

• Project URL: https://gitlab.com/sosy-lab/software/metaval
• Repository URL: https://gitlab.com/sosy-lab/software/cpachecker
• Maintainers:
  • Martin Spiessl
• 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:
  • svcomp24-correctness
  • svcomp24-violation
  • svcomp23
• Literature:
  • MetaVal: Witness Validation via Verification. 2020. DOI: 10.1007/978-3-030-53291-8_10
• Competition Participations:
  • SV-COMP 2024 (Validation of Correctness Witnesses 1.0)
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)

MLB

• Project URL: https://github.com/MLB-SE/Experiment
• Maintainers:
  • Lei Bu
• Supported input languages:
  • Java
• License: MIT
• Supported techniques:
  • Bit-Precise Analysis
  • Portfolio
  • Symbolic Execution
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • svcomp24
  • svcomp24-validation-correctness
  • svcomp23
• Literature:
  • 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
• Presentations:
  • mopsa_svcomp2024.pdf
  • mopsa_svcomp2023.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2024 (Validation of Correctness Witnesses 2.0)
  • SV-COMP 2023 (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:
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Validation of Violation Witnesses 1.0)

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:
  • Bit-Precise Analysis
  • Floating-Point Arithmetics
  • Random Execution
  • Symbolic Execution
  • Targeted Input Generation
• Releases:
  • testcomp24
• Competition Participations:
  • 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:
  • Algorithm Selection
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • Bounded Model Checking
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • k-Induction
  • Lazy Abstraction
  • Numeric Interval Analysis
  • Portfolio
  • Predicate Abstraction
  • Ranking Functions
  • Shape Analysis
• Used frameworks / solvers:
  • CPAchecker
  • JavaSMT
  • MathSAT
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

PIChecker

• Project URL: https://gitlab.com/Lapulatos/pichecker
• Maintainers:
  • Jie Su
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • CEGAR
  • Concurrency Support
  • Interpolation
  • Predicate Abstraction
• Used frameworks / solvers:
  • CPAchecker
  • JavaSMT
  • MathSAT
  • SMTinterpol
• Releases:
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

Pinaka

• Project URL: https://github.com/sbjoshi/Pinaka
• Maintainers:
  • Saurabh Joshi
• Supported input languages:
  • C
• License: BSD-4-Clause
• Supported techniques:
  • Bit-Precise Analysis
  • Bounded Model Checking
  • Symbolic Execution
• Releases:
  • svcomp23
• Literature:
  • Pinaka: Symbolic Execution Meets Incremental Solving (Competition Contribution). 2019. DOI: 10.1007/978-3-030-17502-3_20
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • 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
• Presentations:
  • predatorhp_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

PROTON

• Project URL: https://github.com/kumarmadhukar/term
• Maintainers:
  • Ravindra Metta
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Bounded Model Checking
• Releases:
  • 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 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
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

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 2024 (Test Generation)

SPF

• Project URL: https://github.com/SymbolicPathFinder/jpf-symbc
• Maintainers:
  • Yannic Noller
• Supported input languages:
  • Java
• License: Apache-2.0
• Supported techniques:
  • Concurrency Support
  • Shape Analysis
  • Symbolic Execution
• 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-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

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:
  • svcomp24
• Competition Participations:
  • SV-COMP 2024 (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
• 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 2024 (Verification)

Symbiotic

• Project URL: https://github.com/staticafi/symbiotic
• Maintainers:
  • Martin Jonáš
• Supported input languages:
  • C
• License: MIT
• Supported techniques:
  • Bit-Precise Analysis
  • Concurrency Support
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • k-Induction
  • Numeric Interval Analysis
  • Portfolio
  • Shape Analysis
  • Symbolic Execution
  • Targeted Input Generation
• 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:
  • svcomp24
  • testcomp24
  • svcomp23
  • testcomp23
• Literature:
  • 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
• Presentations:
  • symbiotic_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • Test-Comp 2024 (Test Generation)
  • SV-COMP 2023 (Verification)
  • Test-Comp 2023 (Test Generation)

Symbiotic-Witch

• Project URL: https://github.com/ayazip/witch-klee
• Maintainers:
  • Paulína Ayaziová
• Supported input languages:
  • C
• License: LGPL-3.0-or-later
• Supported techniques:
  • Symbolic Execution
• Releases:
  • svcomp24
  • svcomp23
• 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:
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Validation of Violation Witnesses 1.0)

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:
  • testcomp24
  • testcomp23
• Literature:
  • TestCov: Robust Test-Suite Execution and Coverage Measurement. 2019. DOI: 10.1109/ASE.2019.00105
• Competition Participations:
  • Test-Comp 2024 (Validation of Test Suites)
  • Test-Comp 2023 (Validation of Test Suites)

Theta

• Project URL: https://github.com/ftsrg/theta
• Maintainers:
  • Levente Bajczi
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Algorithm Selection
  • ARG-Based Analysis
  • Bit-Precise Analysis
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • Portfolio
  • Predicate Abstraction
• Releases:
  • svcomp24
  • svcomp23
• Presentations:
  • theta_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (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:
  • Bounded Model Checking
  • Floating-Point Arithmetics
  • Interpolation
  • Symbolic Execution
  • Targeted Input Generation
• Releases:
  • testcomp24
  • svcomp23
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • SV-COMP 2023 (Verification)

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:
  • testcomp24
• Competition Participations:
  • 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.

• Project URL: https://ultimate-pa.org
• Repository URL: https://github.com/ultimate-pa/ultimate
• Maintainers:
  • Matthias Heizmann
  • Dominik Klumpp
  • Frank Schüssele
  • Daniel Dietsch
• Supported input languages:
  • C
• License: LGPL-3.0-or-later
• Supported techniques:
  • Algorithm Selection
  • Automata-Based Analysis
  • Bit-Precise Analysis
  • CEGAR
  • Concurrency Support
  • Interpolation
  • Lazy Abstraction
  • Portfolio
  • Predicate Abstraction
  • Ranking Functions
• Used frameworks / solvers:
  • CVC
  • MathSAT
  • SMTinterpol
  • Ultimate
  • Z3
• Releases:
  • svcomp24-correctness-post-deadline-yaml-wrapper-fix
  • svcomp24
  • svcomp24-correctness
  • svcomp24-violation
  • svcomp23
• Literature:
  • Software Model Checking for People Who Love Automata. 2013. DOI: 10.1007/978-3-642-39799-8_2
  • Ultimate Automizer 2023 (Competition Contribution). 2023. DOI: 10.1007/978-3-031-30820-8_39
• Presentations:
  • uautomizer_svcomp2024.pdf
  • uautomizer_svcomp2023.pdf
• Posters:
  • uautomizer_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2024 (Validation of Correctness Witnesses 1.0)
  • SV-COMP 2024 (Validation of Correctness Witnesses 2.0)
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Verification)

UGemCutter

• Project URL: https://ultimate-pa.org
• Repository URL: https://github.com/ultimate-pa/ultimate
• Maintainers:
  • Matthias Heizmann
  • Dominik Klumpp
  • Frank Schüssele
  • Daniel Dietsch
• Supported input languages:
  • C
• License: LGPL-3.0-or-later
• Supported techniques:
  • Algorithm Selection
  • Automata-Based Analysis
  • Bit-Precise Analysis
  • CEGAR
  • Concurrency Support
  • Interpolation
  • Lazy Abstraction
  • Portfolio
  • Predicate Abstraction
• Used frameworks / solvers:
  • CVC
  • MathSAT
  • SMTinterpol
  • Ultimate
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Literature:
  • Sound sequentialization for concurrent program verification. 2022. DOI: 10.1145/3519939.3523727
  • Ultimate GemCutter and the Axes of Generalization. 2022. DOI: 10.1007/978-3-030-99527-0_35
• Presentations:
  • ugemcutter_svcomp2024.pdf
  • ugemcutter_svcomp2023.pdf
• Posters:
  • ugemcutter_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

UKojak

• Project URL: https://ultimate-pa.org
• Repository URL: https://github.com/ultimate-pa/ultimate
• Maintainers:
  • Matthias Heizmann
  • Dominik Klumpp
  • Frank Schüssele
  • Daniel Dietsch
• Supported input languages:
  • C
• License: LGPL-3.0-or-later
• Supported techniques:
  • Bit-Precise Analysis
  • CEGAR
  • Interpolation
  • Lazy Abstraction
  • Predicate Abstraction
• Used frameworks / solvers:
  • SMTinterpol
  • Ultimate
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Presentations:
  • ukojak_svcomp2024.pdf
• Posters:
  • ukojak_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

UTaipan

• Project URL: https://ultimate-pa.org
• Repository URL: https://github.com/ultimate-pa/ultimate
• Maintainers:
  • Matthias Heizmann
  • Dominik Klumpp
  • Frank Schüssele
  • Daniel Dietsch
• Supported input languages:
  • C
• License: LGPL-3.0-or-later
• Supported techniques:
  • Algorithm Selection
  • Automata-Based Analysis
  • Bit-Precise Analysis
  • CEGAR
  • Concurrency Support
  • Explicit-Value Analysis
  • Interpolation
  • Lazy Abstraction
  • Numeric Interval Analysis
  • Portfolio
  • Predicate Abstraction
• Used frameworks / solvers:
  • CVC
  • MathSAT
  • SMTinterpol
  • Ultimate
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Presentations:
  • utaipan_svcomp2023.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

UTestGen

• Project URL: https://ultimate.informatik.uni-freiburg.de
• Repository URL: https://github.com/ultimate-pa/ultimate
• Maintainers:
  • Max Barth
• Supported input languages:
  • C
• License: LGPL-3.0-or-later
• Supported techniques:
  • Automata-Based Analysis
  • CEGAR
  • Interpolation
  • Portfolio
• Used frameworks / solvers:
  • Ultimate
• Releases:
  • testcomp24
• Presentations:
  • utestgen_testcomp2024.pdf
• Competition Participations:
  • Test-Comp 2024 (Test Generation)

VeriAbs

• Project URL: https://www.tcs.com
• Repository URL: https://gitlab.com/sosy-lab/sv-comp/archives-2023/-/raw/svcomp23/2023/veriabs.zip
• Maintainers:
  • Priyanka Darke
• Supported input languages:
  • C
• License: Other
• Supported techniques:
  • Algorithm Selection
  • Bounded Model Checking
  • CEGAR
  • Evolutionary Algorithms
  • Explicit-Value Analysis
  • k-Induction
  • Numeric Interval Analysis
  • Portfolio
• Used frameworks / solvers:
  • CPAchecker
  • CProver
  • MiniSAT
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

VeriAbsL

• Project URL: https://www.tcs.com
• Repository URL: https://gitlab.com/sosy-lab/sv-comp/archives-2023/-/raw/svcomp23/2023/veriabsl.zip
• Maintainers:
  • Priyanka Darke
• Supported input languages:
  • C
• License: Other
• Supported techniques:
  • Algorithm Selection
  • Bounded Model Checking
  • CEGAR
  • Evolutionary Algorithms
  • Explicit-Value Analysis
  • k-Induction
  • Numeric Interval Analysis
  • Portfolio
• Used frameworks / solvers:
  • CPAchecker
  • CProver
  • MiniSAT
  • Z3
• Releases:
  • svcomp24
  • svcomp23
• Presentations:
  • veriabsl_svcomp2024.pdf
  • veriabsl_svcomp2023.pdf
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

VeriFuzz

• Project URL: https://www.tcs.com
• Maintainers:
  • Raveendra Kumar Medicherla
• Supported input languages:
  • C
• License: LicenseRef-TCSEvaluationLicense
• Supported techniques:
  • Bounded Model Checking
  • Evolutionary Algorithms
  • Explicit-Value Analysis
  • Floating-Point Arithmetics
  • Guidance by Coverage Measures
  • Numeric Interval Analysis
  • Random Execution
• Releases:
  • svcomp23
• Presentations:
  • verifuzz_testcomp2023.pdf
  • verifuzz_svcomp2023.pdf
• Competition Participations:
  • SV-COMP 2023 (Verification)

VeriOover

• Project URL: https://github.com/PaperSheeper/VeriOover-SV
• Maintainers:
  • HaiPeng Qu
• Supported input languages:
  • C
• License: MIT
• Releases:
  • svcomp23
• Competition Participations:
  • SV-COMP 2024 (Verification)
  • SV-COMP 2023 (Verification)

WASP-C

• Project URL: https://github.com/wasp-platform/wasp
• Maintainers:
  • Filipe Marques
• Supported input languages:
  • C
• License: Apache-2.0
• Supported techniques:
  • Floating-Point Arithmetics
  • Random Execution
  • Symbolic Execution
• Releases:
  • testcomp23
• Competition Participations:
  • Test-Comp 2024 (Test Generation)
  • Test-Comp 2023 (Test Generation)

WIT4JAVA

• Project URL: https://github.com/Anthonysdu/wit4java
• Maintainers:
  • Tong Wu
• Supported input languages:
  • Java
• License: BSD-4-Clause
• Releases:
  • svcomp23
• Literature:
  • Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution). 2022. DOI: 10.1007/978-3-030-99527-0_36
• Competition Participations:
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2023 (Validation of Violation Witnesses 1.0)

Witch

• Project URL: https://github.com/ayazip/witch-klee
• Maintainers:
  • Paulína Ayaziová
• Supported input languages:
  • C
• License: LGPL-3.0-or-later
• Supported techniques:
  • Symbolic Execution
• Releases:
  • svcomp24
• Literature:
  • Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 (Competition Contribution). 2024. DOI: 10.1007/978-3-031-57256-2_18
• Presentations:
  • witch_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Validation of Violation Witnesses 2.0)

WitnessLint

• Project URL: https://github.com/sosy-lab/sv-witnesses
• Maintainers:
  • Marian Lingsch-Rosenfeld
• Supported input languages:
  • C
  • Java
• License: Apache-2.0
• Releases:
  • svcomp24-correctness-graphml
  • svcomp24-violation-graphml
  • svcomp24-correctness-yaml
  • svcomp24-violation-yaml
• Presentations:
  • witnesslint_svcomp2024.pdf
• Competition Participations:
  • SV-COMP 2024 (Validation of Correctness Witnesses 1.0)
  • SV-COMP 2024 (Validation of Correctness Witnesses 2.0)
  • SV-COMP 2024 (Validation of Violation Witnesses 1.0)
  • SV-COMP 2024 (Validation of Violation Witnesses 2.0)