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

SV-COMP 2022 (Verification)

• AProVE (KoAT+LoAT)

SV-COMP 2017 (Verification)

• BLAST

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

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