Synthesis of Heap-Manipulating Programs from Separation Logic
-
Updated
Apr 18, 2023 - Scala
Synthesis of Heap-Manipulating Programs from Separation Logic
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).
Hoare Type Theory
An interpreter for an imperative language and a Hoare logic prover
Hoare logic for classroom demonstration
A web-based graphical proof assistant for LK and Hoare logic.
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
Extensible HAHA transpiler.
Synthesis with Read-Only Borrows
A toolkit for the creation of correct-by-construction arithmetic languages.
MIRROR of https://codeberg.org/catseye/Samovar : Model worlds using propositions and run simulations in them
Write readable Hoare style proof outlines for imperative programs in Agda.
Things that are needed for formally verifying a system
Hoare Type Theory
Verification Condition Generator for a Simple Imperative Language and a Guarded Command Language
Agda proof of soundness of Hoare Logic for a simple toy language
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
Calco Python API implementation. Contract-based approach to declaratively specify distributed dataflows
A Vagrant box with the Hoare Advanced Homework Assistant (HAHA) all set up and ready to go.
Add a description, image, and links to the hoare-logic topic page so that developers can more easily learn about it.
To associate your repository with the hoare-logic topic, visit your repo's landing page and select "manage topics."