GitHub topics: program-verification
AeneasVerif/aeneas
A verification toolchain for Rust programs
Language: OCaml - Size: 8.35 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 253 - Forks: 24
BinaryAnalysisPlatform/bap
Binary Analysis Platform
Language: OCaml - Size: 8.27 MB - Last synced at: 3 days ago - Pushed at: 4 days ago - Stars: 2,124 - Forks: 277
AeneasVerif/charon
Interface with the rustc compiler for the purpose of program verification
Language: Rust - Size: 5.78 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 130 - Forks: 19
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.
Language: Python - Size: 80.7 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 41 - Forks: 6
lisa-analyzer/lisa
📚 a modular easy to use Library for Static Analysis aiming at multi-language analysis
Language: Java - Size: 8.68 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 57 - Forks: 35
staticafi/symbiotic
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
Language: Python - Size: 2.13 MB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 320 - Forks: 57
thufv/CMinor-Verifier
2022 年春季学期清华大学《软件分析与验证》课程实验平台 (Lab for Software Analysis and Verification, 2022 Spring, Tsinghua University)
Language: C# - Size: 1.31 MB - Last synced at: 3 days ago - Pushed at: about 1 month ago - Stars: 205 - Forks: 22
tribbloid/shapesafe
SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory
Language: Scala - Size: 7.81 MB - Last synced at: 13 days ago - Pushed at: about 1 year ago - Stars: 32 - Forks: 4
SaswatPadhi/LoopInvGen 📦
Generates loop invariants for program verification
Language: OCaml - Size: 3.91 MB - Last synced at: 2 months ago - Pushed at: about 4 years ago - Stars: 60 - Forks: 20
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]
Language: Coq - Size: 49.8 KB - Last synced at: 13 days ago - Pushed at: 9 months ago - Stars: 31 - Forks: 2
PSS1998/MicroViper-Verifier
A deductive program verification tool for MicroViper programming language
Language: Rust - Size: 94.7 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
hopv/rethfl
ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types
Language: OCaml - Size: 1.63 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0
sun-wendy/DafnyBench
DafnyBench: A Benchmark for Formal Software Verification
Language: Dafny - Size: 5.65 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 15 - Forks: 3
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
Language: Agda - Size: 876 KB - Last synced at: about 2 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0
gabriel-fallen/verification-in-lean4
Examples and exercises related to formal program verification in Lean 4.
Language: Lean - Size: 2.93 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0
seahorn/sea-cut
C/C++ refactoring tool for library abstractions
Language: C++ - Size: 97.7 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 2 - Forks: 0
Chronosymbolic/Chronosymbolic-Learning
Artifact for paper "Chronosymbolic: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning" in Python
Language: Python - Size: 9.13 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 7 - Forks: 0
Mondego/dafny-synthesis
Towards AI-Assisted Synthesis of Verified Dafny Methods
Language: Dafny - Size: 778 KB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 26 - Forks: 0
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)
Language: Haskell - Size: 387 KB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 0 - Forks: 0
VincenzoArceri/rust-lisa
Rust frontend for LiSA
Language: Java - Size: 20.6 MB - Last synced at: about 1 year ago - Pushed at: almost 3 years ago - Stars: 8 - Forks: 0
Flunzmas/gym-autokey
An OpenAI gym environment for automated rule-based deductive program verification in KeY.
Language: Java - Size: 41.1 MB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 6 - Forks: 0
PL-ML/code2inv
Code2Inv: Learning Loop Invariants for Program Verification
Language: SMT - Size: 35.1 MB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 76 - Forks: 22
utpalbora/LLOV
LLOV: LLVM OpenMP Verifier - : A Fast Static Data-Race Checker for OpenMP Programs
Language: C++ - Size: 296 MB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 19 - Forks: 5
Sophietje/Verification-Tool-Overview
Information about verification tools. Browse the data at https://slebok.github.io/proverb/
Language: Python - Size: 1.06 MB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 13 - Forks: 2
BinaryAnalysisPlatform/bap-python
BAP python bindings
Language: Python - Size: 67.4 KB - Last synced at: 6 months ago - Pushed at: over 1 year ago - Stars: 20 - Forks: 12
aionescu/uu-mpsv-gcl-verifier
GCL verification tool based on predicate transformers
Language: Haskell - Size: 729 KB - Last synced at: 29 days ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0
Jacopo00811/02141_Computer_Science_Modelling
02141 Computer Science Modelling Spring 23 DTU
Language: F# - Size: 15.2 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
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.
Language: OCaml - Size: 28.8 MB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 11 - Forks: 9
SatyendraBanjare/Type-Theory-notes 📦
Report on advancements in Type Theory and application of Program Verification
Language: TeX - Size: 9.51 MB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 0
adamalston/comp550 📦
[sp20] Algorithms and Analysis. Formal specification and verification of programs. Techniques of algorithm analysis. Problem-solving paradigms. Survey of algorithms.
Size: 5.32 MB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0
utpalbora/OmpSCR_v2.0
Clone of OmpSCR v2.0 with modifications
Language: Fortran - Size: 310 KB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0
viperproject/voila
Voila is proof outline checker for fine-grained concurrency verification
Language: Scala - Size: 87.7 MB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 2
co-dan/SeLoC
Strong non-interference for fine-grained concurrent programs
Language: Coq - Size: 358 KB - Last synced at: 18 days ago - Pushed at: about 3 years ago - Stars: 3 - Forks: 0
EileenFeng/Verify-Dijkstras-Algorithm-in-Idris
A verification program that proves Dijkstra's algorithm correctness written in Idris.
Language: TeX - Size: 12 MB - Last synced at: almost 2 years ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
utpalbora/drb_fortran
DataRaceBench 1.2 kernels written in FORTRAN for LLVM-IR based data race detection tools
Language: Fortran - Size: 143 KB - Last synced at: about 1 year ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 1
sdasgup3/PLDI19-ArtifactEvaluation
Artifact Evaluation, PLDI'19
Size: 656 KB - Last synced at: 13 days ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 0
IITH-Compilers/drb_fortran
DataRaceBench 1.2 kernels written in FORTRAN for LLVM-IR based data race detection tools
Language: Fortran - Size: 78.1 KB - Last synced at: 10 days ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0
