
Smallfoot
 Referenced in 51 articles
[sw09787]
 Smallfoot: Modular automatic assertion checking with separation logic. Separation logic is a program logic ... tool for checking certain lightweight separation logic specifications. The assertions describe the shapes of data ... oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what...

VeriFast
 Referenced in 64 articles
[sw07705]
 program verifier. This note describes a separationlogicbased approach for the specification and verification ... abstract representation of memory as a separation logic assertion. Folding or unfolding abstract predicate assertions...

Datalog
 Referenced in 289 articles
[sw20023]
 beginning of logic programming, but it became prominent as a separate area around 1977 when...

HIP
 Referenced in 29 articles
[sw09786]
 heap manipulating programs. HIP is a separation logic based automated verification system for a simple ... will construct a set of separation logic proof obligations in the form of formula implications ... which are sent to the SLEEK separation logic prover. SLEEK is a fully automatic prover ... separation logic with frame inferring capability...

cminor
 Referenced in 19 articles
[sw09739]
 Separation Logic for SmallStep cminor. cminor is a midlevel imperative programming language; there ... reasoning and we have designed a Separation Logic for cminor. In this paper, we give ... checked proof of soundness of our Separation Logic. This is the first largescale machine ... checked proof of a Separation Logic w.r.t. a smallstep semantics. The work presented...

Slide
 Referenced in 20 articles
[sw28542]
 SLIDE  Separation Logic with Inductive Definitions. Automatabased entailment checking for Separation Logic with Inductive ... prototype tool for checking entailment in Separation Logic with userprovided inductive definitions of recursive...

jStar
 Referenced in 32 articles
[sw11261]
 symbolic execution and abstraction using separation logic. The proposed technology has been implemented...

URDME
 Referenced in 25 articles
[sw10400]
 construction. The core simulation routines are logically separated from the model building interface and written...

Cyclist
 Referenced in 21 articles
[sw18519]
 algorithms have been integrated, focusing on Separation Logic with inductively defined predicates. For information...

Predator
 Referenced in 18 articles
[sw07396]
 were originally inspired by works on separation logic with higherorder list predicates, but they...

Charge!
 Referenced in 10 articles
[sw22731]
 Charge! A framework for higherorder separation logic in Coq. We present a comprehensive ... shallow embedding of a higherorder separation logic for a subset of Java ... abstraction similar to penandpaper separationlogic proof outlines. In particular, the tactics allow...

Curry
 Referenced in 45 articles
[sw08981]
 combine the currently separated research efforts of the functional and logic programming communities...

Find
 Referenced in 86 articles
[sw21614]
 intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally...

SOLAVOF
 Referenced in 44 articles
[sw24125]
 used for calculations involving two fluids separated by a sharp interface. In either case ... program. Its logical parts are isolated in separate subroutines, and numerous special features have been...

MONA
 Referenced in 133 articles
[sw06170]
 reductions, DAGification, guided tree automata, threevalued logic, eager minimization, BDDbased automata representations ... quantify their respective effects by experimenting with separate versions of the MONA tool that...

Separation Logic
 Referenced in 7 articles
[sw28549]
 Separation Logic Framework for Imperative HOL. We provide a framework for separationlogic based correctness...

VerCors
 Referenced in 7 articles
[sw11259]
 VerCors project we use permissionbased separation logic to reason about multithreaded Java programs ... discuss in particular how we use the logic to use different implementations of synchronisers ... Concretely, we illustrate how permissionbased separation logic is suitable to verify functional correctness properties...

Viper
 Referenced in 9 articles
[sw15038]
 verification techniques based on firstorder logic specifications has benefitted greatly from verification infrastructures such ... suited to verification techniques based on separation logic and other permission logics, because they...

GRASShopper
 Referenced in 6 articles
[sw23304]
 properties. The logic supports mixing of separation logic and firstorder logic assertions, yielding expressive...

Mercury
 Referenced in 69 articles
[sw08333]
 delivers efficiency far in excess of existing logic programming systems, and close to conventional programming ... largescale program development, allowing modularity, separate compilation, and numerous optimization/time tradeoffs...