Static analyzer for C/C++ based on the theory of Abstract Interpretation.
- Updated
- C++
#
software-verification
Here are 66 public repositories matching this topic...
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
llvm verification symbolic-execution instrumentation slice program-verification software-verification klee slicing llvm-ir verification-toolchain program-slicing
- Updated
- Python
Static Analyzer for LLVM bitcode based on Abstract Interpretation. **Update**: clam is still actively maintained. Please use branch dev14.
- Updated
- C
CPAchecker, the Configurable Software-Verification Platform (read-only mirror)
- Updated
- Java
Static analysis framework for C
c static-code-analysis static-analysis ocaml program-analysis software-verification abstract-interpretation race-detection race-conditions
- Updated
- OCaml
Collection of Verification Tasks (MOVED, please follow the link)
- Updated
Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.
coq ideas startup z3 formal-methods sat-solver entrepreneurship software-verification smt-solver research-paper formal-verification quantum-programming-language research-data research-software-engineering programming-language-theory ideasworthsharing
- Updated
The CBMC starter kit makes it easy to add CBMC verification to a software project.
- Updated
- Python
Teaching and Learning Software Verification via SVF
- Updated
- C++
Map2Check: Finding Software Vulnerabilities
- Updated
- SWIG
DPLL(T)-based Verification tool for DNNs
abstraction sat-solver software-verification ai-safety robustness dpll adversarial-attacks robustness-verification dnn-verification ai-assurance neural-network-veri
- Updated
- Python
Read-only mirror of the Klever Git repository
c static-analysis verification specification model-checking formal-methods software-verification formal-verification formal-specification
- Updated
- Python
Multi-agent coding orchestrator with quorum consensus and formal verification (TLA+, Alloy, PRISM) for Claude Code, OpenCode, and Gemini CLI. Fewer hallucinations, fewer blind spots, mathematically proven protocols.
mcp opencode devtools quorum formal-methods alloy software-verification multi-agent-systems tla-plus autonomous-agent ai-agent meta-prompting gemini-cli claude-code context-engineering
- Updated
- JavaScript
An Exchange Format for Verification Witnesses (MOVED, please follow the link)
- Updated
- Python
Information to reproduce results from SV-COMP (MOVED, please follow the link)
- Updated
LSVerifier - Large Systems Verifier
model-checking software-verification formal-verification bounded-model-checking c-language open-source-software security-vulnerabilities
- Updated
- Python
Formalisation of the linear lambda calculus in Coq
- Updated
- Coq
A self-verifying proof that the Thiele Machine is a universal model of computation which strictly contains the Turing Machine as a blind, special case. All open source.
python computer-science information-theory computational-geometry formal-methods turing-machine software-verification epistemology z3-smt-solver computer-science-theory proof-complexity thiele-machine sight-debt philosophy-of-computation church-turing-thesis
- Updated
- C++
Prototype functional programming language with refinement types, powered by Inox
- Updated
- Scala
Improve this page
Add a description, image, and links to the software-verification topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the software-verification topic, visit your repo's landing page and select "manage topics."