hoare-logic topic

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

ilyasergey

Synthesis of Heap-Manipulating Programs from Separation Logic

TyGuS

Hoare Type Theory

imdea-software

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

codersguild

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

coq-community

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

AD1024

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

catseye

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

proof-tree-builder