Tools for Formal Methods: Competitions

SV-COMP 2027 (Verification)

• 2LS (inactive)
• aise (inactive)
• AProVE (KoAT+LoAT) (inactive)
• BRICK (inactive)
• Bubaak (inactive)
• Bubaak-SpLit (inactive)
• CBMC (inactive)
• CoOpeRace (meta_tool, inactive)
• CPA-BAM-BnB (inactive)
• CPA-BAM-SMG (inactive)
• CPAchecker (inactive)
• CPV (inactive)
• Crux (inactive)
• CSeq (inactive)
• Dartagnan (inactive)
• DASA (inactive)
• Deagle (inactive)
• EmergenTheta (inactive)
• ESBMC-incr (inactive)
• ESBMC-kind (inactive)
• Gazer-Theta (inactive)
• GDart (inactive)
• Goblint (inactive)
• Goblint-Par (unqualified, inactive)
• Goblitch (inactive)
• Graves-CPA (inactive, meta_tool)
• Hornix (inactive)
• iekke (inactive)
• Java-Ranger (inactive)
• JayHorn (inactive)
• JBMC (inactive)
• JLiSA (inactive)
• Korn (inactive)
• MLB (inactive)
• Mopsa (inactive)
• MuVal (inactive)
• Nacpa (meta_tool, inactive)
• OGChecker (inactive)
• PeSCo-CPA (inactive, meta_tool)
• PredatorHP (inactive)
• PROTON (inactive)
• PySvLib-CHC (inactive)
• RacerF (inactive)
• Re3ver (inactive)
• ReFuncTion (inactive)
• SEAL (inactive)
• SV-sanitizers (inactive)
• SVF-SVC (inactive)
• SvLibChecker (inactive)
• SWAT (inactive)
• Symbiotic (inactive)
• Theta (inactive)
• Thorn (inactive)
• UAutomizer (inactive)
• UGemCutter (inactive)
• UKojak (inactive)
• UParalizer (inactive)
• UTaipan (inactive)
• VeriAbs (inactive)
• VeriAbsL (inactive)
• WitnessMap (auxiliary)

SV-COMP 2026 (Verification)

• 2LS (inactive)
• aise
• AProVE (KoAT+LoAT)
• BRICK
• Bubaak (inactive)
• Bubaak-SpLit (inactive)
• CBMC (inactive)
• COASTAL (inactive)
• CoOpeRace (meta_tool)
• CPA-BAM-BnB (inactive)
• CPA-BAM-SMG (inactive)
• CPAchecker
• CPALockator (inactive)
• CPV
• Crux (inactive)
• CSeq
• Dartagnan
• DASA
• Deagle
• DIVINE (inactive)
• EBF (inactive)
• EmergenTheta
• ESBMC-incr
• ESBMC-kind
• Frama-C-SV (inactive)
• Gazer-Theta (inactive)
• GDart
• GDart-LLVM (inactive)
• Goblint
• Goblint-Par (unqualified)
• Goblitch
• Graves-CPA (inactive, meta_tool)
• Hornix
• iekke
• Infer (inactive)
• Java-Ranger (inactive)
• JayHorn
• JBMC
• JDart (inactive)
• JLiSA
• Korn
• Lazy-CSeq (inactive)
• LF-checker (inactive)
• Locksmith (inactive)
• MLB
• Mopsa
• MuVal
• Nacpa (meta_tool)
• OGChecker
• PeSCo-CPA (inactive, meta_tool)
• PIChecker (inactive)
• Pinaka (inactive)
• PredatorHP (inactive)
• PROTON
• PySvLib-CHC
• RacerF
• Re3ver
• ReFuncTion
• SEAL
• SPF (inactive)
• SV-sanitizers
• SVF-SVC
• SvLibChecker
• SWAT
• Symbiotic
• Theta
• Thorn
• UAutomizer
• UGemCutter
• UKojak
• UParalizer
• UTaipan
• VeriAbs (inactive)
• VeriAbsL (inactive)
• VeriOover (inactive)
• WitnessMap (auxiliary)

SV-COMP 2025 (Verification)

• 2LS
• aise
• AProVE (KoAT+LoAT)
• BRICK
• Bubaak
• Bubaak-SpLit
• CBMC (inactive)
• COASTAL (inactive)
• CoOpeRace (meta_tool)
• CPA-BAM-BnB (inactive)
• CPA-BAM-SMG (inactive)
• CPAchecker
• CPALockator (inactive)
• CPV
• Crux (inactive)
• CSeq (inactive)
• Dartagnan
• Deagle
• DIVINE (inactive)
• EBF (inactive)
• EmergenTheta
• ESBMC-incr
• ESBMC-kind
• Frama-C-SV (inactive)
• Gazer-Theta (inactive)
• GDart
• GDart-LLVM (inactive)
• Goblint
• Graves-CPA (inactive, meta_tool)
• Hornix
• Infer (inactive)
• Java-Ranger
• JayHorn (inactive)
• JBMC
• JDart (inactive)
• Korn
• Lazy-CSeq (inactive)
• LF-checker (inactive)
• Locksmith (inactive)
• MLB
• Mopsa
• Nacpa (meta_tool)
• PeSCo-CPA (inactive, meta_tool)
• PIChecker (inactive)
• Pinaka (inactive)
• PredatorHP (inactive)
• PROTON
• RacerF
• SPF (inactive)
• SV-sanitizers
• SVF-SVC
• SWAT
• Symbiotic
• Theta
• Thorn
• UAutomizer
• UGemCutter
• UKojak
• UTaipan
• VeriAbs (inactive)
• VeriAbsL (inactive)
• VeriOover (inactive)
• WitnessMap (auxiliary)

SV-COMP 2024 (Verification)

• 2LS
• aise
• BRICK
• Bubaak
• Bubaak-SpLit
• CBMC (inactive)
• COASTAL (inactive)
• CoVeriTeam-Verifier-AlgoSelection (inactive, meta_tool)
• CoVeriTeam-Verifier-ParallelPortfolio (inactive, meta_tool)
• CPA-BAM-BnB (inactive)
• CPA-BAM-SMG (inactive)
• CPAchecker
• CPALockator (inactive)
• CPV
• Crux (inactive)
• CSeq (inactive)
• Dartagnan
• Deagle
• DIVINE (inactive)
• EBF
• EmergenTheta
• ESBMC-incr (inactive)
• ESBMC-kind
• Frama-C-SV
• Gazer-Theta (inactive)
• GDart
• GDart-LLVM (inactive)
• Goblint
• Graves-CPA (inactive, meta_tool)
• Graves-Par (inactive, meta_tool)
• Infer (inactive)
• Java-Ranger (inactive)
• JayHorn
• JBMC
• JDart (inactive)
• Korn
• Lazy-CSeq (inactive)
• LF-checker (inactive)
• Locksmith (inactive)
• MLB
• Mopsa
• PeSCo-CPA (inactive, meta_tool)
• PIChecker (inactive)
• Pinaka (inactive)
• PredatorHP
• PROTON
• RELAY-SV (unqualified)
• SPF (inactive)
• SV-sanitizers
• SWAT
• Symbiotic
• Theta
• UAutomizer
• UGemCutter
• UKojak
• UTaipan
• VeriAbs
• VeriAbsL
• VeriOover (inactive)

SV-COMP 2023 (Verification)

• 2LS
• BRICK
• Bubaak
• CBMC
• COASTAL (inactive)
• CoVeriTeam-Verifier-AlgoSelection (inactive, meta_tool)
• CoVeriTeam-Verifier-ParallelPortfolio (inactive, meta_tool)
• CPA-BAM-BnB (inactive)
• CPA-BAM-SMG (inactive)
• CPAchecker
• CPALockator (inactive)
• Crux (inactive)
• CSeq (inactive)
• Dartagnan
• Deagle
• DIVINE (inactive)
• EBF
• ESBMC-incr (inactive)
• ESBMC-kind
• Frama-C-SV
• Gazer-Theta (inactive)
• GDart
• GDart-LLVM
• Goblint
• Graves-CPA (meta_tool)
• Graves-Par (inactive, meta_tool)
• Infer (inactive)
• Java-Ranger
• JayHorn (inactive)
• JBMC
• JDart (inactive)
• Korn
• Lazy-CSeq (inactive)
• LF-checker
• Locksmith
• MLB
• Mopsa
• PeSCo-CPA (meta_tool)
• PIChecker
• Pinaka (inactive)
• PredatorHP (inactive)
• SPF (inactive)
• Symbiotic
• Theta
• TracerX
• UAutomizer
• UGemCutter
• UKojak
• UTaipan
• VeriAbs
• VeriAbsL
• VeriFuzz
• VeriOover

SAT Competition 2025 (Main)

• AMSAT
• AMSAT_RGC (inactive)
• CaDiCaL
• Cadical_ESA (inactive)
• hCaD-pbva
• hKis-pbva
• IsaSAT
• kissat
• Kissat_MAB_Binary (inactive)
• Kissat_MAB_ESA (inactive)

SAT Competition 2024 (Main)

• AMSAT
• AMSAT_RGC
• BreakID-Kissat
• CaDiCaL
• Cadical_ESA
• hCaD-bva
• hCaD-pbva
• hKis-bva
• hKis-pbva
• IsaSAT
• kissat
• Kissat_MAB-DC
• Kissat_MAB_Binary
• Kissat_MAB_ESA

SAT Competition 2023 (Main)

• AMSAT
• BreakID-Kissat
• CaDiCaL
• Cadical_ESA
• hKis-bva
• hKis-pbva
• IsaSAT
• kissat
• Kissat_MAB_Binary
• Kissat_MAB_ESA

SV-COMP 2022 (Verification)

• AProVE (KoAT+LoAT)
• SMACK (inactive)

SV-COMP 2017 (Verification)

• BLAST
• CIVL
• Forester
• HIP/SLEEK
• SMACK
• Yogar-CBMC

SAT Competition 2022 (Main)

• CaDiCaL
• Cadical_ESA
• hCaD-bva
• hCaD-pbva
• hKis-bva
• hKis-pbva
• IsaSAT
• kissat
• Kissat_MAB_ESA

SAT Competition 2021 (Main)

• CaDiCaL
• hCaD-bva
• hCaD-pbva
• hKis-bva
• hKis-pbva
• kissat

SAT Competition 2020 (Main)

• CaDiCaL
• kissat

SAT Competition 2018 (Main)

• CaDiCaL

SAT Competition 2017 (Main)

• CaDiCaL

SV-COMP 2016 (Verification)

• CIVL
• Forester
• HIP/SLEEK
• SMACK
• VVT

SV-COMP 2018 (Verification)

• Forester
• VIAP
• Yogar-CBMC

SV-COMP 2015 (Verification)

• Forester
• HIP/SLEEK
• SMACK

SV-COMP 2021 (Verification)

• SMACK

SV-COMP 2019 (Verification)

• SMACK
• VIAP
• Yogar-CBMC

SV-COMP 2020 (Verification)

• Yogar-CBMC

SAT Competition 2017 (Agile)

• CaDiCaL

SAT Competition 2022 (NoLimits)

• BreakID-Kissat
• CaDiCaL
• hCaD-bva
• hCaD-pbva
• hKis-bva
• hKis-pbva
• IsaSAT

SAT Competition 2021 (NoLimits)

• CaDiCaL
• hCaD-bva
• hCaD-pbva
• hKis-bva
• hKis-pbva

SAT Competition 2020 (NoLimits)

• CaDiCaL

SAT Competition 2018 (NoLimits)

• CaDiCaL

SAT Competition 2017 (NoLimits)

• CaDiCaL

SAT Competition 2023 (Parallel)

• hKis-bva
• hKis-pbva

Test-Comp 2027 (Test Generation)

• AFL-to-Test-Case (inactive)
• cetfuzz (inactive)
• CoVeriTest (inactive)
• ESBMC-incr (inactive)
• ESBMC-kind (inactive)
• FDSE (inactive)
• Fizzer (inactive)
• FuSeBMC (inactive)
• FuSeBMC-AI (inactive)
• HybridTiger (inactive)
• KLEE (inactive)
• KLEEF (inactive)
• Owi (inactive)
• PRTest (inactive)
• Rizzer (inactive)
• Sikraken (inactive)
• Symbiotic (inactive)
• TracerX (inactive)
• TracerX-WP (inactive)
• UTestGen (inactive)
• WASP-C (inactive)

Test-Comp 2026 (Test Generation)

• AFL-to-Test-Case
• cetfuzz (inactive)
• CoVeriTest
• ESBMC-incr
• ESBMC-kind
• FDSE
• Fizzer
• FuSeBMC
• FuSeBMC-AI (inactive)
• HybridTiger (inactive)
• KLEE (inactive)
• KLEEF (inactive)
• Owi (inactive)
• PRTest
• Rizzer (inactive)
• Sikraken
• Symbiotic
• TracerX (inactive)
• TracerX-WP (inactive)
• UTestGen
• WASP-C (inactive)

Test-Comp 2025 (Test Generation)

• cetfuzz (inactive)
• CoVeriTest
• ESBMC-incr
• ESBMC-kind
• FDSE
• Fizzer
• FuSeBMC
• FuSeBMC-AI (inactive)
• HybridTiger (inactive)
• KLEE (inactive)
• KLEEF
• Owi (inactive)
• PRTest
• Rizzer (inactive)
• Sikraken
• Symbiotic
• TracerX
• TracerX-WP
• UTestGen
• WASP-C (inactive)

Test-Comp 2024 (Test Generation)

• cetfuzz
• CoVeriTest
• ESBMC-kind (inactive)
• FDSE
• Fizzer
• FuSeBMC
• FuSeBMC-AI
• HybridTiger (inactive)
• KLEE (inactive)
• KLEEF
• Legion (inactive)
• Legion/SymCC (inactive)
• Owi
• PRTest
• Rizzer
• Symbiotic
• TracerX
• TracerX-WP
• UTestGen
• WASP-C (inactive)

Test-Comp 2023 (Test Generation)

• CoVeriTest
• ESBMC-kind
• FuSeBMC
• FuSeBMC-AI
• HybridTiger (inactive)
• KLEE (inactive)
• Legion (inactive)
• Legion/SymCC
• PRTest
• Symbiotic
• WASP-C

SAT Competition 2022 (Anniversary)

• CaDiCaL
• hKis-bva
• hKis-pbva
• IsaSAT

Test-Comp 2024 (Validation of Test Suites)

• TestCov

Test-Comp 2023 (Validation of Test Suites)

• TestCov

SV-COMP 2027 (Validation of SV-LIB Witnesses v1)

• PySvLib-Linter (auxiliary)
• PySvLib-Validator (inactive)

SV-COMP 2026 (Validation of SV-LIB Witnesses v1)

• PySvLib-Linter (auxiliary)
• PySvLib-Validator

SV-COMP 2027 (Validation of Violation Witnesses v1)

• ConcurrentWitness2Test (inactive)
• CPA-witness2test (inactive)
• CPAchecker (inactive)
• CProver-witness2test (inactive)
• Dartagnan (inactive)
• GWIT (inactive)
• MetaVal (inactive)
• NITWIT (inactive)
• Symbiotic-Witch (inactive)
• UAutomizer (inactive)
• Wit4Java (inactive)
• WitnessLint (auxiliary)

SV-COMP 2026 (Validation of Violation Witnesses v1)

• ConcurrentWitness2Test
• CPA-witness2test (inactive)
• CPAchecker
• CProver-witness2test (inactive)
• Dartagnan
• GWIT (inactive)
• MetaVal (inactive)
• NITWIT (inactive)
• Symbiotic-Witch (inactive)
• UAutomizer
• Wit4Java
• WitnessLint (auxiliary)

SV-COMP 2025 (Validation of Violation Witnesses v1)

• ConcurrentWitness2Test
• CPA-witness2test (inactive)
• CPAchecker
• CProver-witness2test (inactive)
• Dartagnan
• GWIT (inactive)
• MetaVal
• NITWIT (inactive)
• Symbiotic-Witch
• UAutomizer
• Wit4Java
• WitnessLint (auxiliary)

SV-COMP 2024 (Validation of Violation Witnesses v1)

• ConcurrentWitness2Test
• CPA-witness2test
• CPAchecker
• CProver-witness2test (inactive)
• Dartagnan
• GWIT
• MetaVal
• NITWIT
• Symbiotic-Witch
• UAutomizer
• Wit4Java (inactive)
• WitnessLint (auxiliary)

SV-COMP 2023 (Validation of Violation Witnesses v1)

• CPA-witness2test
• CProver-witness2test
• GWIT
• NITWIT
• Symbiotic-Witch
• Wit4Java

SV-COMP 2027 (Validation of Violation Witnesses v2)

• CPAchecker (inactive)
• MetaVal (inactive)
• Theta (inactive)
• UAutomizer (inactive)
• Witch (inactive)
• WitnessLint (auxiliary)

SV-COMP 2026 (Validation of Violation Witnesses v2)

• CPAchecker
• MetaVal
• Theta
• UAutomizer
• Witch
• WitnessLint (auxiliary)

SV-COMP 2025 (Validation of Violation Witnesses v2)

• CPAchecker
• MetaVal
• UAutomizer
• Witch
• WitnessLint (auxiliary)

SV-COMP 2024 (Validation of Violation Witnesses v2)

• CPAchecker
• Witch
• WitnessLint (auxiliary)

SV-COMP 2027 (Validation of Correctness Witnesses v2)

• CPAchecker (inactive)
• Goblint (inactive)
• LIV (inactive)
• MetaVal (inactive)
• Mopsa (inactive)
• Theta (inactive)
• UAutomizer (inactive)
• UGemCutter (inactive)
• UReferee (inactive)
• WitnessLint (auxiliary)

SV-COMP 2027 (Validation of Correctness Witnesses v1)

• CPAchecker (inactive)
• JCWIT (inactive)
• LIV (inactive)
• MetaVal (inactive)
• UAutomizer (inactive)
• UReferee (inactive)
• WitnessLint (auxiliary)

SV-COMP 2026 (Validation of Correctness Witnesses v2)

• CPAchecker
• Goblint
• LIV
• MetaVal
• Mopsa
• Theta
• UAutomizer
• UGemCutter
• UReferee
• WitnessLint (auxiliary)

SV-COMP 2026 (Validation of Correctness Witnesses v1)

• CPAchecker (inactive)
• JCWIT (inactive)
• LIV (inactive)
• MetaVal (inactive)
• UAutomizer (inactive)
• UReferee (inactive)
• WitnessLint (auxiliary)

SV-COMP 2025 (Validation of Correctness Witnesses v1)

• CPAchecker
• JCWIT (inactive)
• LIV
• MetaVal
• UAutomizer
• UReferee
• WitnessLint (auxiliary)

SV-COMP 2025 (Validation of Correctness Witnesses v2)

• CPAchecker
• Goblint
• LIV
• MetaVal
• MetaVal++
• Mopsa
• UAutomizer
• UReferee
• WitnessLint (auxiliary)

SV-COMP 2024 (Validation of Correctness Witnesses v1)

• CPAchecker
• JCWIT
• LIV
• MetaVal
• UAutomizer
• WitnessLint (auxiliary)

SV-COMP 2024 (Validation of Correctness Witnesses v2)

• CPAchecker
• Goblint
• Mopsa
• UAutomizer
• WitnessLint (auxiliary)

Test-Comp 2027 (Validation of Test Suites GCC Formatted)

• TestCov (inactive)

Test-Comp 2026 (Validation of Test Suites GCC Formatted)

• TestCov

Test-Comp 2025 (Validation of Test Suites GCC Formatted)

• TestCov

Test-Comp 2027 (Validation of Test Suites Clang Formatted)

• TestCoCa (inactive)
• TestCov (inactive)

Test-Comp 2026 (Validation of Test Suites Clang Formatted)

• TestCoCa
• TestCov

Test-Comp 2027 (Validation of Test Suites GCC Unformatted)

• TestCov (inactive)

Test-Comp 2026 (Validation of Test Suites GCC Unformatted)

• TestCov

Test-Comp 2025 (Validation of Test Suites Clang Formatted)

• TestCov

Test-Comp 2025 (Validation of Test Suites GCC Unformatted)

• TestCov

Test-Comp 2027 (Validation of Test Suites Clang Unformatted)

• TestCov (inactive)

Test-Comp 2026 (Validation of Test Suites Clang Unformatted)

• TestCov

Test-Comp 2025 (Validation of Test Suites Clang Unformatted)

• TestCov