The Wayback Machine - https://web.archive.org/web/20230627210025/https://github.com/topics/program-verification

#

program-verification

Here are 28 public repositories matching this topic...

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

Updated Jun 9, 2023
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

Updated Apr 30, 2023
Python

thufv / CMinor-Verifier

2022 年春季学期清华大学《软件分析与验证》课程实验平台

course-project program-verification

Updated Aug 26, 2022
C#

PL-ML / code2inv

Code2Inv: Learning Loop Invariants for Program Verification

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

Updated Jan 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

Updated Jan 22, 2021
OCaml

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

template coq program-verification template-repository

Updated Jun 23, 2023
Coq

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

Updated Apr 20, 2023
Java

dig

dynaroars / dig

DIG is a a dynamic invariant generation tool that infers program invariants or properties over (i) program execution traces or (ii) program source code (C, Java, Java bytecode). DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations. DIG…

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

Updated May 30, 2023
Python

BinaryAnalysisPlatform / bap-python

BAP python bindings

python reverse-engineering bap program-analysis program-verification

Updated Jan 24, 2023
Python

ManuelLerchner / fpv-tutorial-SS23

Materialien für das FPV-Tutorium im Sommersemester 2023

pdf functional-programming tum slides program-verification

Updated Jun 19, 2023
OCaml

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

Updated Oct 5, 2022
C++

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

Updated Jun 27, 2023
Scala

Sophietje / Verification-Tool-Overview

Information about existing verification tools. You can browse the data at https://slebok.github.io/proverb/

tools verification formal-methods program-verification formal-verification

Updated Apr 11, 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

Updated Mar 12, 2019
OCaml

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

Updated Nov 13, 2020
Java

VincenzoArceri / rust-lisa

Rust frontend for LiSA

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

Updated Jul 22, 2022
Java

co-dan / SeLoC

Strong non-interference for fine-grained concurrent programs

coq iris type-system program-verification separation-logic coq-library noninterference

Updated Mar 11, 2022
Coq

aionescu / uu-mpsv-gcl-verifier

GCL verification tool based on predicate transformers

haskell z3 program-verification wlp

Updated Nov 12, 2022
Haskell

utpalbora / drb_fortran

DataRaceBench 1.2 kernels written in FORTRAN for LLVM-IR based data race detection tools

fortran openmp program-verification llvm-ir race-detection data-race-detection dataracebench-fortran-kernels

Updated May 28, 2020
Fortran

utpalbora / OmpSCR_v2.0

Clone of OmpSCR v2.0 with modifications

openmp shared-memory program-verification sword archer race-detection parallel-programming shared-memory-parallel helgrind data-race-detection llov romp valgrind-drd

Updated May 16, 2020
Fortran

Improve this page

Add a description, image, and links to the program-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 the program-verification topic, visit your repo's landing page and select "manage topics."