Lecture notes for a short course on proving/programming in Coq via SSReflect.

Synthesis of Heap-Manipulating Programs from Separation Logic

Hoare Type Theory

Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).

A web-based graphical proof assistant for LK and Hoare logic.

Python3 auto-active verification library (migrated to an Intel project)

A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]

MIRROR of https://codeberg.org/catseye/Samovar : Model worlds using propositions and run simulations in them

Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

Pyrefine – python code checker based on Hoare logic

A verifier for a simple imperative language powered by Z3

Hoare logic for classroom demonstration

A toolkit for the creation of correct-by-construction arithmetic languages.

Verification Condition Generator for a Simple Imperative Language and a Guarded Command Language

Mini-language for program verification using Hoare logic

A Study in Implementing Functional Programming Languages

Synthesis with Read-Only Borrows

Write readable Hoare style proof outlines for imperative programs in Agda.

Things that are needed for formally verifying a system

Hoare Type Theory