separation-logic
There are 42 repositories under separation-logic topic.
TyGuS/suslik
Synthesis of Heap-Manipulating Programs from Separation Logic
DistributedComponents/disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
imdea-software/htt
Hoare Type Theory
utwente-fmt/vercors
The VerCors verification toolset for verifying parallel and concurrent software
logsem/aneris
Program logic for developing and verifying distributed systems
imdea-software/fcsl-pcm
Partial Commutative Monoids
katamaran-project/katamaran
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.
iwilare/formal-methods
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
logsem/clutch
Probabilistic separation logics for verifying higher-order probabilistic programs.
star-finder/jpf-star
Test input generation using separation logic
TyGuS/ssl-htt
Coq tactics for certification of the results of SSL-based program synthesis via Hoare Type Theory.
SpencerL-Y/SESL
A Symbolic Executor based on Separaton Logic
tchajed/coq-sep-logic
Separation logic library for Coq
SoundVerification/wireguard
Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol
tchajed/seplogic-demo
Demos for lecture on Separation Logic by O'Hearn from CACM 2019.
TDacik/Astral
Decision procedure for strong-separation logic
verse-lab/sisyphus
Mostly Automated Proof Repair for Verified Libraries
wllqwzx/seplogic
An implementation of separation logic in Coq
co-dan/SeLoC
Strong non-interference for fine-grained concurrent programs
logsem/VMSL
Verifying FF-A hypercalls using VMSL.
sl-comp/sl-comp.github.io
Competition of Solvers for Separation Logic
star-finder/jpf-costar
Test input generation using separation logic
PKUTCS/CSVerifi
An implementation of the logic for verifying the correctness of cloud storage system in Coq
BinksZhang/CBS-Verification
A verification tool developed in Coq for analyzing cloud block storage
ilyasergey/htt
Hoare Type Theory
jolmari/boilerplate-separated-aspnet-core-angular
Sample Angular-enabled ASP.NET Core application with separated backend and frontend structure
logsem/AxSL
AxSL, a concurrent separation logic for Arm's relaxed concurrency
Niols/GSoC17
Google Summer of Code 2017 – Verification and Testing of Heap-based Programs with Symbolic PathFinder
Olavhaasie/hoare-proof-outlines
Write readable Hoare style proof outlines for imperative programs in Agda.
supermartian/le-verification
Things that are needed for formally verifying a system
TyGuS/robosuslik
Synthesis with Read-Only Borrows
viperproject/voila
Voila is proof outline checker for fine-grained concurrency verification
PKUTCS-CBS/CBS-Verification
A verification tool developed in Coq for analyzing cloud block storage
verse-lab/arboreta
Mechanised Reasoning about Array-Based Trees in Separation Logic
marcoantoniocorallo/Failure-Analyzer
FAILURE Analyzer is a tool for static analysis and bug detection which implements Separation Sufficient Incorrectness Logic (SSIL) as the base logic on which the analysis is driven.
paulrav/ravapolishtech
this is paulrav ict solutions