hoare-logic
There are 32 repositories under hoare-logic topic.
ilyasergey/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
TyGuS/suslik
Synthesis of Heap-Manipulating Programs from Separation Logic
imdea-software/htt
Hoare Type Theory
codersguild/Software-Analysis-PAVT
Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).
proof-tree-builder/proof-tree-builder.github.io
A web-based graphical proof assistant for LK and Hoare logic.
AD1024/veripy
Python3 auto-active verification library (migrated to an Intel project)
coq-community/hoare-tut
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
catseye/Samovar
MIRROR of https://codeberg.org/catseye/Samovar : Model worlds using propositions and run simulations in them
iwilare/formal-methods
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
vdimir/py-refinement-lambda
Pyrefine – python code checker based on Hoare logic
maciejpirog/grzb
A verifier for a simple imperative language powered by Z3
shraiysh/hoare-logic
Hoare logic for classroom demonstration
benmandrew/cavalry
Mini-language for program verification using Hoare logic
ferhaterata/vc-gen
Verification Condition Generator for a Simple Imperative Language and a Guarded Command Language
lambdacasserole/capriccio
A toolkit for the creation of correct-by-construction arithmetic languages.
pqnelson/ml
A Study in Implementing Functional Programming Languages
dvcarrillo/concurrencia-basica
Ejemplos básicos de programación concurrente y paralelismo.
ilyasergey/htt
Hoare Type Theory
kammitama5/OnProgrammingforCorrectness
LaTeX and matlab files for this course
Olavhaasie/hoare-proof-outlines
Write readable Hoare style proof outlines for imperative programs in Agda.
piotr-lewandowski/hoare-triples
Agda proof of soundness of Hoare Logic for a simple toy language
supermartian/le-verification
Things that are needed for formally verifying a system
TyGuS/robosuslik
Synthesis with Read-Only Borrows
flame-stream/calco
Contract-based approach to declaratively specify distributed dataflows
flame-stream/palco
Calco Python API implementation. Contract-based approach to declaratively specify distributed dataflows
TyGuS/htt
Hoare Type Theory
bor0/hoare-hask
Paper: Tutorial implementation of Hoare logic in Haskell
cister-labs/fvoca2223
Web page hosting the pedagocical material prepared in the scope of the FVOCA class of the MESCC MSc
lambdacasserole/haha-box
A Vagrant box with the Hoare Advanced Homework Assistant (HAHA) all set up and ready to go.
lambdacasserole/haha-parser
Unofficial, handwritten parser aimed at transpilation of the HAHA language.
lambdacasserole/haha-transpiler
Extensible HAHA transpiler.
SauzeauYannis/LS-Projet
An interpreter for an imperative language and a Hoare logic prover