program-verification
There are 41 repositories under program-verification topic.
BinaryAnalysisPlatform/bap
Binary Analysis Platform
AeneasVerif/aeneas
A verification toolchain for Rust programs
staticafi/symbiotic
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
thufv/CMinor-Verifier
2022 年春季学期清华大学《软件分析与验证》课程实验平台 (Lab for Software Analysis and Verification, 2022 Spring, Tsinghua University)
AeneasVerif/charon
Interface with the rustc compiler for the purpose of program verification
PL-ML/code2inv
Code2Inv: Learning Loop Invariants for Program Verification
lisa-analyzer/lisa
📚 a modular easy to use Library for Static Analysis aiming at multi-language analysis
SaswatPadhi/LoopInvGen
Generates loop invariants for program verification
dynaroars/dig
DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.
Mondego/dafny-synthesis
[FSE-2024] Towards AI-Assisted Synthesis of Verified Dafny Methods
sun-wendy/DafnyBench
DafnyBench: A Benchmark for Formal Software Verification
rocq-community/coq-program-verification-template
Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
tribbloid/shapesafe
SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory
Sophietje/Verification-Tool-Overview
Information about verification tools. Browse the data at https://slebok.github.io/proverb/
BinaryAnalysisPlatform/bap-python
BAP python bindings
utpalbora/LLOV
LLOV: LLVM OpenMP Verifier - : A Fast Static Data-Race Checker for OpenMP Programs
kappelmann/eidi2_repetitorium_tum
This repository is intended for the Functional Programming and Verification (EIDI2) revision courses 2016 and 2017 at the Technical University of Munich.
Chronosymbolic/Chronosymbolic-Learning
Artifact for paper "Chronosymbolic: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning" in Python
VincenzoArceri/rust-lisa
Rust frontend for LiSA
Flunzmas/gym-autokey
An OpenAI gym environment for automated rule-based deductive program verification in KeY.
co-dan/SeLoC
Strong non-interference for fine-grained concurrent programs
aionescu/uu-mpsv-gcl-verifier
GCL verification tool based on predicate transformers
RU-Automated-Reasoning-Group/VEL
TACAS'23: Verification-guided Programmatic Controller Synthesis
sdasgup3/PLDI19-ArtifactEvaluation
Artifact Evaluation, PLDI'19
seahorn/sea-cut
C/C++ refactoring tool for library abstractions
adamalston/comp550
[sp20] Algorithms and Analysis. Formal specification and verification of programs. Techniques of algorithm analysis. Problem-solving paradigms. Survey of algorithms.
hopv/rethfl
ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types
utpalbora/drb_fortran
DataRaceBench 1.2 kernels written in FORTRAN for LLVM-IR based data race detection tools
utpalbora/OmpSCR_v2.0
Clone of OmpSCR v2.0 with modifications
viperproject/voila
Voila is proof outline checker for fine-grained concurrency verification
giorgiosld/Static-Analysis-and-Program-Verification
This repo contains the material about the course "Static Analysis and Program Verification" supplied in the Master Degree (LM-18) at the University of Camerino
jaksicf/program-verification-eth
My solution for project 1 for the "Program Verification" course at ETH Zurich (ETHZ) (https://www.pm.inf.ethz.ch/education/courses/program-verification.html)
JhonTabio/OpenJML-Specs
Contains the specifications for the Java language used by OpenJML.
ayeshakhzafar/CodeMirror
A Web-based tool that helps analyze the correctness and equivalence of programs using formal methods.
gabriel-fallen/verification-in-lean4
Examples and exercises related to formal program verification in Lean 4.
ioncakephper/contract-shield-cli
A CLI tool that processes @pre, @post, and @invariant tags in functions, classes, and methods within a source file. It generates a modified version of the source code that automatically validates input conditions (@pre), result conditions (@post), and invariant conditions (@invariant).