goblint/analyzer

Static analysis framework for C

Language: OCaml - Size: 38.7 MB - Last synced at: about 21 hours ago - Pushed at: about 21 hours ago - Stars: 200 - Forks: 77

NASA-SW-VnV/ikos

Static analyzer for C/C++ based on the theory of Abstract Interpretation.

Language: C++ - Size: 5.04 MB - Last synced at: 4 days ago - Pushed at: about 1 month ago - Stars: 2,944 - Forks: 203

sosy-lab/cpachecker

CPAchecker, the Configurable Software-Verification Platform (read-only mirror)

Language: SWIG - Size: 871 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 237 - Forks: 90

ldv-klever/klever

Read-only mirror of the Klever Git repository

Language: Python - Size: 162 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 21 - Forks: 14

adilanwar2399/ESBMC-ibmc

The ESBMC ibmc (Invariant Based Model Checking) Tool.

Language: C - Size: 327 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 6 - Forks: 1

model-checking/cbmc-starter-kit

The CBMC starter kit makes it easy to add CBMC verification to a software project.

Language: Python - Size: 1.42 MB - Last synced at: 7 days ago - Pushed at: about 2 months ago - Stars: 45 - Forks: 22

SVF-tools/Teaching-Software-Verification

Teaching and Learning Software Verification via SVF

Language: C++ - Size: 10.8 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 33 - Forks: 23

staticafi/symbiotic

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

Language: Python - Size: 2.13 MB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 320 - Forks: 57

seahorn/clam

Static Analyzer for LLVM bitcode based on Abstract Interpretation. **Update**: clam is still actively maintained. Please use branch dev14.

Language: C - Size: 4.02 MB - Last synced at: 16 days ago - Pushed at: about 1 year ago - Stars: 279 - Forks: 39

Benestar/rust-model-checker

A Model Checker in Rust

Language: Rust - Size: 43.9 KB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 4 - Forks: 0

hbgit/Map2Check

Map2Check: Finding Software Vulnerabilities

Language: SWIG - Size: 1.02 GB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 28 - Forks: 9

soarlab/rust-benchmarks

Rust software verification benchmarks

Language: Rust - Size: 173 KB - Last synced at: 17 days ago - Pushed at: about 1 year ago - Stars: 4 - Forks: 2

dynaroars/neuralsat

DPLL(T)-based Verification tool for DNNs

Language: Python - Size: 628 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 14 - Forks: 0

Stumble/TrustCoq

Formal Verification on NDN trust schema

Language: Coq - Size: 116 KB - Last synced at: 3 days ago - Pushed at: about 8 years ago - Stars: 2 - Forks: 0

sarmadiali98/LinguaFranca-to-Rebeca

Lingua Franca codes and their equivalent Rebeca code

Size: 197 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 1 - Forks: 0

SatyendraBanjare/plt-formal-methods-resources

Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.

Size: 3.24 MB - Last synced at: 15 days ago - Pushed at: over 5 years ago - Stars: 55 - Forks: 1

janislley/LSVerifier

LSVerifier - Large Systems Verifier

Language: Python - Size: 22.4 MB - Last synced at: 12 days ago - Pushed at: about 1 year ago - Stars: 11 - Forks: 3

sarbojit4/nidhugg Fork of nidhugg/nidhugg

Nidhugg is a bug-finding tool which targets bugs caused by concurrency and relaxed memory consistency in concurrent programs. It is particularly useful for programs written in C/pthreads. Currently Nidhugg supports the SC, TSO, PSO, POWER and ARM (partial) memory models.

Language: C - Size: 9.3 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 1

gpetiot/Frama-C-StaDy 📦

Static & Dynamic Verification of C programs

Language: OCaml - Size: 2.3 MB - Last synced at: 22 days ago - Pushed at: over 5 years ago - Stars: 9 - Forks: 3

Hacker-Code-J/Software-Verification

Language: TeX - Size: 6.61 MB - Last synced at: about 1 month ago - Pushed at: 9 months ago - Stars: 1 - Forks: 0

martinchapman/learning-errors

Abstractly represent software error traces as finite automata.

Language: C++ - Size: 15.9 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 2 - Forks: 0

mirkootter/lean-mt

Lean4-Framework to reason about multithreaded algorithms

Language: Lean - Size: 102 KB - Last synced at: about 1 year ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

PosteruOle/2023_Analysis_Compound_Unit

This repository contains an analysis of a Compound Unit student project. Analysis was done using tools for static and dynamic software verification. The repository is created for the purpose of Software Verification master's studies course at the Faculty of Mathematics.

Language: HTML - Size: 13.6 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

supleed2/ELEC70056-HSV-CW1

About Coursework 1 for ELEC70056: Hardware and Software Verification, Software Component - Verification of code using Dafny and the theorem-prover Isabelle

Language: Isabelle - Size: 10.8 MB - Last synced at: 12 months ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

polywit/polywit

🌍 A poly-language execution-based violation-witness validator

Language: Python - Size: 1.15 MB - Last synced at: 9 days ago - Pushed at: over 1 year ago - Stars: 4 - Forks: 0

smtifahim/EFBO-Ontology-Repository

This repository contains three ontology files relevant to the Event-Based Functional Behaviour Ontology (EFBO) project as part of a Software Engineering thesis.

Language: HTML - Size: 280 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

michaelsproul/honours-thesis

4th Year Honours Thesis on Programming Language Semantics

Language: TeX - Size: 29.7 MB - Last synced at: 8 days ago - Pushed at: almost 9 years ago - Stars: 1 - Forks: 0

sosy-lab/sv-witnesses 📦

An Exchange Format for Verification Witnesses (MOVED, please follow the link)

Language: Python - Size: 326 KB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 18 - Forks: 9

Edivad99/WAI

Language: F# - Size: 64.5 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 1

sosy-lab/sv-comp 📦

Information to reproduce results from SV-COMP (MOVED, please follow the link)

Size: 624 KB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 14 - Forks: 51

covercig/covercig.github.io

Language: HTML - Size: 2.12 MB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0

sosy-lab/sv-benchmarks 📦

Collection of Verification Tasks (MOVED, please follow the link)

Size: 3.45 GB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 186 - Forks: 168

ArmanOzcan18/probabilistic-full-program-induction

full-program induction technique extended to probabilistic programs

Language: C - Size: 24.4 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

ivan-ristovic/LICC 📦

Language invariant AST abstraction with APIs to create, visualize or compare ASTs

Language: C# - Size: 28.8 MB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0

ivan-ristovic/BBE 📦

Software Verification course project - Fixing bugs using a working example as a specification

Language: Java - Size: 29.7 MB - Last synced at: over 1 year ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 1

divyeshunadkat/divyeshunadkat.github.io

Personal Webpage

Language: HTML - Size: 19.9 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

Edivad99/WhileAbstractInterpreter

Language: F# - Size: 229 KB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

flynnWhelehan/thirdYear

Third year @ RHUL (out of 5) Mostly lab and exercise work from third year. All modules for the year listed in topics. See https://github.com/flynnWhelehan/softwareVerification repo (currently private) for the second term module which is a two-person project.

Language: Haskell - Size: 62.8 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

michaelsproul/dblib-linear

Formalisation of the linear lambda calculus in Coq

Language: Coq - Size: 81.1 KB - Last synced at: 8 days ago - Pushed at: over 6 years ago - Stars: 10 - Forks: 0

SEL4PROJ/cakeml-bake

CakeML build tool

Language: Rust - Size: 71.3 KB - Last synced at: 8 days ago - Pushed at: almost 6 years ago - Stars: 2 - Forks: 0

LedgerProject/safepkt_rust-verification-tools

SafePKT Flavor of RVT (a collection of tools/libraries to support both static and dynamic verification of Rust programs.)

Language: Rust - Size: 2.88 MB - Last synced at: 12 months ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

tomas-dias/msc-sweng

Projects and assignments done during Master's Degree course in Informatics Engineering, with specialisation in Software Engineering, at Faculty of Sciences of the University of Lisbon.

Language: Java - Size: 34.1 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

viperproject/voila

Voila is proof outline checker for fine-grained concurrency verification

Language: Scala - Size: 87.7 MB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 2

osterhoutan-UofU/alloy-viz

(my verification project for cs5110 / cs6110) A vscode extension that adds live visualizations of alloy type structures to vscode. (also includes some basic some basic langauge support)

Language: TypeScript - Size: 2.63 MB - Last synced at: 4 months ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 0

romac/oxid-light

Prototype functional programming language with refinement types, powered by Inox

Language: Scala - Size: 6.84 KB - Last synced at: 15 days ago - Pushed at: almost 7 years ago - Stars: 7 - Forks: 1

D33pBlue/While-DS-interpreter

An interpreter for Denotational Semantics of While language

Language: Python - Size: 984 KB - Last synced at: about 2 years ago - Pushed at: about 7 years ago - Stars: 1 - Forks: 1