
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...

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

VeriFast
 Referenced in 52 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...

HIP
 Referenced in 22 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...

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

Slide
 Referenced in 16 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...

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

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

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

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

Charge!
 Referenced in 8 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...

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

SOLAVOF
 Referenced in 39 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 114 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 6 articles
[sw28549]
 Separation Logic Framework for Imperative HOL. We provide a framework for separationlogic based correctness...

VerCors
 Referenced in 5 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 6 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...

Mercury
 Referenced in 65 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...

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