Topic: "hoare-logic"
ilyasergey/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Language: Coq - Size: 6.47 MB - Last synced at: 21 days ago - Pushed at: almost 4 years ago - Stars: 164 - Forks: 19
TyGuS/suslik
Synthesis of Heap-Manipulating Programs from Separation Logic
Language: Scala - Size: 8.07 MB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 121 - Forks: 19
imdea-software/htt
Hoare Type Theory
Language: Coq - Size: 549 KB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 75 - Forks: 5
codersguild/Software-Analysis-PAVT
Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).
Language: Boogie - Size: 21.9 MB - Last synced at: about 1 month ago - Pushed at: about 2 years ago - Stars: 37 - Forks: 6
proof-tree-builder/proof-tree-builder.github.io
A web-based graphical proof assistant for LK and Hoare logic.
Language: JavaScript - Size: 5.39 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 24 - Forks: 2
AD1024/veripy
Python3 auto-active verification library (migrated to an Intel project)
Language: Python - Size: 90.8 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 20 - Forks: 0
rocq-community/hoare-tut
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
Language: Coq - Size: 71.3 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 20 - Forks: 2
catseye/Samovar
MIRROR of https://codeberg.org/catseye/Samovar : Model worlds using propositions and run simulations in them
Language: Python - Size: 168 KB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 16 - Forks: 2
iwilare/formal-methods
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
Language: Agda - Size: 32.2 KB - Last synced at: 10 months ago - Pushed at: over 2 years ago - Stars: 14 - Forks: 1
vdimir/py-refinement-lambda
Pyrefine – python code checker based on Hoare logic
Language: Python - Size: 78.1 KB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 9 - Forks: 0
maciejpirog/grzb
A verifier for a simple imperative language powered by Z3
Language: Racket - Size: 943 KB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 4 - Forks: 0
shraiysh/hoare-logic
Hoare logic for classroom demonstration
Language: C++ - Size: 50.8 KB - Last synced at: almost 2 years ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 2
lambdacasserole/capriccio
A toolkit for the creation of correct-by-construction arithmetic languages.
Language: Java - Size: 33.2 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 2 - Forks: 1
ferhaterata/vc-gen
Verification Condition Generator for a Simple Imperative Language and a Guarded Command Language
Language: C++ - Size: 19.4 MB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 2 - Forks: 0
pqnelson/ml
A Study in Implementing Functional Programming Languages
Language: C - Size: 104 KB - Last synced at: 7 days ago - Pushed at: almost 6 years ago - Stars: 2 - Forks: 0
TyGuS/robosuslik
Synthesis with Read-Only Borrows
Language: Scala - Size: 1.2 MB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 1
supermartian/le-verification
Things that are needed for formally verifying a system
Size: 1000 Bytes - Last synced at: about 1 year ago - Pushed at: almost 8 years ago - Stars: 1 - Forks: 0
kammitama5/OnProgrammingforCorrectness
LaTeX and matlab files for this course
Language: TeX - Size: 109 KB - Last synced at: 7 months ago - Pushed at: about 8 years ago - Stars: 1 - Forks: 0
ilyasergey/htt Fork of imdea-software/htt
Hoare Type Theory
Language: Coq - Size: 123 KB - Last synced at: about 2 years ago - Pushed at: about 8 years ago - Stars: 1 - Forks: 0
dvcarrillo/concurrencia-basica
Ejemplos básicos de programación concurrente y paralelismo.
Language: C++ - Size: 36.1 KB - Last synced at: about 2 years ago - Pushed at: over 9 years ago - Stars: 1 - Forks: 0
piotr-lewandowski/hoare-triples
Agda proof of soundness of Hoare Logic for a simple toy language
Language: Agda - Size: 10.7 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0
benmandrew/cavalry
Mini-language for program verification using Hoare logic
Language: OCaml - Size: 95.7 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
cister-labs/fvoca2223
Web page hosting the pedagocical material prepared in the scope of the FVOCA class of the MESCC MSc
Language: HTML - Size: 2.11 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
SauzeauYannis/LS-Projet 📦
An interpreter for an imperative language and a Hoare logic prover
Language: OCaml - Size: 468 KB - Last synced at: 4 months ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 2
bor0/hoare-hask
Paper: Tutorial implementation of Hoare logic in Haskell
Language: TeX - Size: 871 KB - Last synced at: 3 days ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
lambdacasserole/haha-transpiler
Extensible HAHA transpiler.
Language: Java - Size: 36.1 KB - Last synced at: about 1 month ago - Pushed at: about 4 years ago - Stars: 0 - Forks: 1
lambdacasserole/haha-parser
Unofficial, handwritten parser aimed at transpilation of the HAHA language.
Language: Java - Size: 130 KB - Last synced at: about 1 month ago - Pushed at: about 4 years ago - Stars: 0 - Forks: 0
flame-stream/calco
Contract-based approach to declaratively specify distributed dataflows
Size: 1.95 KB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 0 - Forks: 0
flame-stream/palco
Calco Python API implementation. Contract-based approach to declaratively specify distributed dataflows
Language: Python - Size: 7.81 KB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 0 - Forks: 0
TyGuS/htt Fork of imdea-software/htt
Hoare Type Theory
Language: Coq - Size: 217 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0
lambdacasserole/haha-box
A Vagrant box with the Hoare Advanced Homework Assistant (HAHA) all set up and ready to go.
Language: Ruby - Size: 15.6 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0