Movatterモバイル変換

Skip to content

#

program-verification

Here are 39 public repositories matching this topic...

Language:All

Filter by language

All39 OCaml5 Python5 Java4 C++3 Fortran3 Coq2 Haskell2 Rust2 Scala2 TeX2

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

UpdatedMar 17, 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

UpdatedMar 19, 2025
Python

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

UpdatedMar 18, 2025
OCaml

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

UpdatedMar 17, 2025
Rust

PL-ML /code2inv

Code2Inv: Learning Loop Invariants for Program Verification

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

UpdatedJan 26, 2021
SMT

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

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

UpdatedFeb 18, 2025
Java

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

UpdatedSep 5, 2024
Python

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

UpdatedMar 24, 2024
Scala

coq-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

sun-wendy /DafnyBench

DafnyBench: A Benchmark for Formal Software Verification

benchmark language-model dafny program-verification formal-verification

UpdatedDec 12, 2024
Dafny

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

VincenzoArceri /rust-lisa

Rust frontend for LiSA

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

UpdatedJul 22, 2022
Java

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

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