Synthesis of Heap-Manipulating Programs from Separation Logic
-
Updated
Apr 18, 2023 - Scala
#
separation-logic
Here are 43 public repositories matching this topic...
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
-
Updated
Jul 26, 2024 - Coq
Hoare Type Theory
-
Updated
May 5, 2025 - Coq
The VerCors verification toolset for verifying parallel and concurrent software
c java opencl concurrency openmp verification viper parallelism software-analysis separation-logic vercors-toolset
-
Updated
May 1, 2025 - Scala
Program logic for developing and verifying distributed systems
-
Updated
Apr 21, 2025 - Coq
Partial Commutative Monoids
-
Updated
May 5, 2025 - Coq
Probabilistic separation logics for verifying higher-order probabilistic programs.
-
Updated
May 5, 2025 - Coq
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
-
Updated
Aug 25, 2022 - Agda
Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.
-
Updated
Apr 25, 2025 - < 10000 span class="repo-language-color" style="background-color: #d0b68c"> Coq
An automated deductive program verifier based on concurrent separation logic
concurrency verification concurrent-programming concurrent-data-structure separation-logic automated-reasoning deductive-reasoning intermediate-verification-languages
-
Updated
May 4, 2025 - OCaml
Test input generation using separation logic
-
Updated
Jul 5, 2019 - Java
Mostly Automated Proof Repair for Verified Libraries
ocaml coq higher-order-functions formal-verification separation-logic pldi-artifact curry-howard-isomorphism proof-repair invariant-inference
-
Updated
Jun 1, 2023 - OCaml
A Symbolic Executor based on Separaton Logic
-
Updated
Mar 27, 2024 - SWIG
Coq tactics for certification of the results of SSL-based program synthesis via Hoare Type Theory.
-
Updated
Jul 5, 2021 - Coq
Solver for separation logic(s) based on translation to SMT
-
Updated
Apr 1, 2025 - OCaml
An implementation of separation logic in Coq
-
Updated
May 19, 2017 - Coq
Demos for lecture on Separation Logic by O'Hearn from CACM 2019.
-
Updated
Sep 26, 2024 - Coq
Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol
implementation tamarin separation-logic protocol-verification symbolic-security automated-verification
-
Updated
Dec 9, 2022 - Haskell
Verifying FF-A hypercalls using VMSL.
-
Updated
Apr 14, 2023 - Coq
Improve this page
Add a description, image, and links to the separation-logic topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the separation-logic topic, visit your repo's landing page and select "manage topics."