#

program-verification

Here are 25 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 Dec 24, 2022
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 Dec 23, 2022
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

palmskog / coq-program-verification-template

Template project for program verification in Coq

coq program-verification template-repository

Updated Aug 27, 2022
Coq

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 Dec 20, 2022
Python

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 Dec 22, 2022
Java

BinaryAnalysisPlatform / bap-python

BAP python bindings

python reverse-engineering bap program-analysis program-verification

Updated Nov 18, 2020
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

Updated Dec 15, 2022
Scala

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

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

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 Dec 5, 2022
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

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

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

sdasgup3 / PLDI19-ArtifactEvaluation

Artifact Evaluation, PLDI'19

x86-64 formal-semantics instruction-semantics program-verification isa-specification

Updated Apr 18, 2020

viperproject / voila

Voila is proof outline checker for fine-grained concurrency verification

concurrency verification formal-methods program-verification software-verification separation-logic fine-grained-concurrency

Updated Apr 10, 2022
Scala

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."