Movatterモバイル変換

Skip to content

#

program-verification

Here are 42 public repositories matching this topic...

Language:All

Filter by language

All42 OCaml5 Python5 Java4 C++3 Fortran3 Rocq Prover2 Haskell2 JavaScript2 Rust2 Scala2

Sort:Most stars

Sort options

Most stars Fewest stars Most forks Fewest forks Recently updated Least recently updated

BinaryAnalysisPlatform /bap

Binary Analysis Platform

emulator security arm mips static-analysis ocaml reverse-engineering disassembler symbolic-execution bap x86 dynamic-analysis binary-analysis instruction-semantics program-analysis taint-analysis powerpc program-verification lifter

UpdatedApr 30, 2025
OCaml

AeneasVerif /aeneas

A verification toolchain for Rust programs

rust compiler ocaml coq rust-lang lean formal-methods proofs program-verification formal-verification fstar hol4 deductive-reasoning

UpdatedNov 5, 2025
OCaml

staticafi /symbiotic

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

UpdatedOct 30, 2025
Python

thufv /CMinor-Verifier

2022 年春季学期清华大学《软件分析与验证》课程实验平台 (Lab for Software Analysis and Verification, 2022 Spring, Tsinghua University)

course-project program-verification

UpdatedMar 10, 2025
C#

AeneasVerif /charon

Interface with the rustc compiler for the purpose of program verification

rust compiler static-analysis rust-lang formal-methods program-verification formal-verification

UpdatedNov 5, 2025
Rust

PL-ML /code2inv

Code2Inv: Learning Loop Invariants for Program Verification

program-verification graph-neural-loop-invariant-generation

UpdatedJan 26, 2021
SMT

lisa

lisa-analyzer /lisa

📚 a modular easy to use Library for Static Analysis aiming at multi-language analysis

java analysis static-analysis analyzer cybersecurity formal-methods lisa static-analyzer program-verification static-analyzers abstract-interpretation

UpdatedNov 6, 2025
Java

SaswatPadhi /LoopInvGen

Generates loop invariants for program verification

synthesis invariants program-verification loop-invariants sygus syntax-guided-synthesis sygus-solver invariant-generation cegis

UpdatedJan 22, 2021
OCaml

Mondego /dafny-synthesis

[FSE-2024] Towards AI-Assisted Synthesis of Verified Dafny Methods

program-synthesis dafny program-verification llms

UpdatedJun 9, 2024
Dafny

dig

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.

machine-learning symbolic-execution dynamic-analysis program-verification loop-invariants invariant-generation specification-mining neural-network-verification

UpdatedMay 24, 2025
Python

sun-wendy /DafnyBench

DafnyBench: A Benchmark for Formal Software Verification

benchmark language-model dafny program-verification formal-verification

UpdatedDec 12, 2024
Dafny

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]

template coq program-verification template-repository

UpdatedJul 31, 2024
Coq

shapesafe

tribbloid /shapesafe

SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory

machine-learning scala linear-algebra type-theory program-verification shape-safety

UpdatedSep 9, 2025
Scala

Sophietje /Verification-Tool-Overview

Information about verification tools. Browse the data athttps://slebok.github.io/proverb/

tools verification formal-methods program-verification formal-verification

UpdatedDec 9, 2023
Python

utpalbora /LLOV

LLOV: LLVM OpenMP Verifier - : A Fast Static Data-Race Checker for OpenMP Programs

fortran llvm static-analysis openmp clang program-verification polly llvm-ir race-detection race-conditions flang data-race race-detector openmp-verification dataracebench-fortran openmp-programs llvm-openmp-verifier race-checker

UpdatedOct 5, 2022
C++

BinaryAnalysisPlatform /bap-python

BAP python bindings

python reverse-engineering bap program-analysis program-verification

UpdatedDec 1, 2023
Python

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.

fpv functional-programming tum ocaml wp technical-university munich program-verification eidi2-revision-course eidi eidi2 eidi-2 revision-course big-step

UpdatedMar 12, 2019
OCaml

Chronosymbolic /Chronosymbolic-Learning

Artifact for paper "Chronosymbolic: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning" in Python

smt program-verification chc

UpdatedAug 4, 2024
Python

VincenzoArceri /rust-lisa

Rust frontend for LiSA

rust static-analysis verification formal-methods lisa static-analyzer program-verification abstract-interpretation

UpdatedJul 22, 2022
Java

Flunzmas /gym-autokey

An OpenAI gym environment for automated rule-based deductive program verification in KeY.

reinforcement-learning verification openai-gym formal-methods program-verification formal-verification gym-environment deductive-reasoning reinforcement-learning-environments

UpdatedNov 13, 2020
Java

Improve this page

Add a description, image, and links to theprogram-verification topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with theprogram-verification topic, visit your repo's landing page and select "manage topics."

[8]ページ先頭

©2009-2025 Movatter.jp