Ecosyste.ms: Repos

An open API service providing repository metadata for many open source software ecosystems.

GitHub topics: program-verification

Repositories

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.6 MB - Last synced: 6 days ago - Pushed: 6 days ago - Stars: 33 - Forks: 6

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: 12 days ago - Pushed: 14 days ago - Stars: 0 - Forks: 0

BinaryAnalysisPlatform/bap

Binary Analysis Platform

Language: OCaml - Size: 8.07 MB - Last synced: 17 days ago - Pushed: 18 days ago - Stars: 1,986 - Forks: 271

Mondego/dafny-synthesis

Towards AI-Assisted Synthesis of Verified Dafny Methods

Language: Dafny - Size: 716 KB - Last synced: 20 days ago - Pushed: 22 days ago - Stars: 21 - Forks: 0

AeneasVerif/charon

Interface with the rustc compiler for the purpose of program verification

Language: Rust - Size: 2.36 MB - Last synced: 27 days ago - Pushed: 27 days ago - Stars: 42 - Forks: 13

AeneasVerif/aeneas

A verification toolchain for Rust programs

Language: OCaml - Size: 5.4 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 112 - Forks: 11

thufv/CMinor-Verifier

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

Language: C# - Size: 1.32 MB - Last synced: about 1 month ago - Pushed: over 1 year ago - Stars: 184 - Forks: 20

hopv/rethfl

ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types

Language: OCaml - Size: 1.63 MB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 0 - Forks: 0

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]

Language: Coq - Size: 44.9 KB - Last synced: about 1 month ago - Pushed: 11 months ago - Stars: 26 - Forks: 2

VincenzoArceri/rust-lisa

Rust frontend for LiSA

Language: Java - Size: 20.6 MB - Last synced: about 2 months ago - Pushed: almost 2 years ago - Stars: 8 - Forks: 0

lisa-analyzer/lisa

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

Language: Java - Size: 7.61 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 35 - Forks: 29

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: about 1 month ago - Pushed: about 2 months ago - Stars: 22 - Forks: 4

staticafi/symbiotic

Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE

Language: Python - Size: 2.11 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 281 - Forks: 54

SaswatPadhi/LoopInvGen

Generates loop invariants for program verification

Language: OCaml - Size: 3.91 MB - Last synced: 7 months ago - Pushed: over 3 years ago - Stars: 52 - Forks: 20

Flunzmas/gym-autokey

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

Language: Java - Size: 41.1 MB - Last synced: 7 months ago - Pushed: over 3 years ago - Stars: 6 - Forks: 0

PL-ML/code2inv

Code2Inv: Learning Loop Invariants for Program Verification

Language: SMT - Size: 35.1 MB - Last synced: 7 months ago - Pushed: over 3 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: 4 months ago - Pushed: over 1 year 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: 9 months ago - Pushed: 10 months ago - Stars: 13 - Forks: 2

sdasgup3/PLDI19-ArtifactEvaluation

Artifact Evaluation, PLDI'19

Size: 656 KB - Last synced: 9 months ago - Pushed: about 4 years ago - Stars: 1 - Forks: 0

BinaryAnalysisPlatform/bap-python

BAP python bindings

Language: Python - Size: 67.4 KB - Last synced: about 2 months ago - Pushed: 6 months ago - Stars: 20 - Forks: 12

Jacopo00811/02141_Computer_Science_Modelling

02141 Computer Science Modelling Spring 23 DTU

Language: F# - Size: 15.2 MB - Last synced: almost 1 year ago - Pushed: almost 1 year 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: about 1 year ago - Pushed: about 5 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: about 1 year ago - Pushed: over 5 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: about 1 year ago - Pushed: about 4 years ago - Stars: 0 - Forks: 0