software-verification
There are 48 repositories under software-verification topic.
NASA-SW-VnV/ikos
Static analyzer for C/C++ based on the theory of Abstract Interpretation.
staticafi/symbiotic
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
seahorn/clam
Static Analyzer for LLVM bitcode based on Abstract Interpretation
sosy-lab/cpachecker
CPAchecker, the Configurable Software-Verification Platform (read-only mirror)
goblint/analyzer
Static analysis framework for C
sosy-lab/sv-benchmarks
Collection of Verification Tasks (MOVED, please follow the link)
SatyendraBanjare/plt-formal-methods-resources
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.
model-checking/cbmc-starter-kit
The CBMC starter kit makes it easy to add CBMC verification to a software project.
SVF-tools/Teaching-Software-Verification
Teaching and Learning Software Verification via SVF
hbgit/Map2Check
Map2Check: Finding Software Vulnerabilities
ldv-klever/klever
Read-only mirror of the Klever Git repository
sosy-lab/sv-witnesses
An Exchange Format for Verification Witnesses (MOVED, please follow the link)
sosy-lab/sv-comp
Information to reproduce results from SV-COMP (MOVED, please follow the link)
dynaroars/neuralsat
DPLL(T)-based Verification tool for DNNs
janislley/LSVerifier
LSVerifier - Large Systems Verifier
michaelsproul/dblib-linear
Formalisation of the linear lambda calculus in Coq
gpetiot/Frama-C-StaDy
Static & Dynamic Verification of C programs
romac/oxid-light
Prototype functional programming language with refinement types, powered by Inox
adilanwar2399/ESBMC-ibmc
The ESBMC ibmc (Invariant Based Model Checking) Tool.
Benestar/rust-model-checker
A Model Checker in Rust
polywit/polywit
🌍 A poly-language execution-based violation-witness validator
ConsistAnts/ConsistAnts
A consistency checker for probabilistic software quality models
soarlab/rust-benchmarks
Rust software verification benchmarks
martinchapman/learning-errors
Abstractly represent software error traces as finite automata.
SEL4PROJ/cakeml-bake
CakeML build tool
Stumble/TrustCoq
Formal Verification on NDN trust schema
D33pBlue/While-DS-interpreter
An interpreter for Denotational Semantics of While language
divyeshunadkat/divyeshunadkat.github.io
Personal Webpage
michaelsproul/honours-thesis
4th Year Honours Thesis on Programming Language Semantics
mirkootter/lean-mt
Lean4-Framework to reason about multithreaded algorithms
Olavhaasie/hoare-proof-outlines
Write readable Hoare style proof outlines for imperative programs in Agda.
sarmadiali98/LinguaFranca-to-Rebeca
Lingua Franca codes and their equivalent Rebeca code
viperproject/voila
Voila is proof outline checker for fine-grained concurrency verification
ArmanOzcan18/probabilistic-full-program-induction
full-program induction technique extended to probabilistic programs
gauthiii/cse565_svvt
CSE 565: Software Verification and Validation @ Arizona State University