Agda proof of soundness of Hoare Logic for a simple toy language
-
Updated
May 12, 2024 - Agda
Agda proof of soundness of Hoare Logic for a simple toy language
Hoare Type Theory
MIRROR of https://codeberg.org/catseye/Samovar : Model worlds using propositions and run simulations in them
Mini-language for program verification using Hoare logic
Synthesis of Heap-Manipulating Programs from Separation Logic
Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).
Web page hosting the pedagocical material prepared in the scope of the FVOCA class of the MESCC MSc
A web-based graphical proof assistant for LK and Hoare logic.
Pyrefine – python code checker based on Hoare logic
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
Write readable Hoare style proof outlines for imperative programs in Agda.
An interpreter for an imperative language and a Hoare logic prover
Python3 auto-active verification library (migrated to an Intel project)
Paper: Tutorial implementation of Hoare logic in Haskell
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Extensible HAHA transpiler.
Unofficial, handwritten parser aimed at transpilation of the HAHA language.
Contract-based approach to declaratively specify distributed dataflows
Calco Python API implementation. Contract-based approach to declaratively specify distributed dataflows
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."