
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 271 articles
[sw20023]
 beginning of logic programming, but it became prominent as a separate area around 1977 when...

VeriFast
 Referenced in 48 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 20 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 15 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 20 articles
[sw10400]
 construction. The core simulation routines are logically separated from the model building interface and written...

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

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

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 78 articles
[sw21614]
 intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally...

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

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

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

MONA
 Referenced in 113 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...

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

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

VeriStar
 Referenced in 3 articles
[sw09393]
 prover for a decidable subset of separation logic. Together with VeriSmall, a provedsound Smallfoot ... tightly integrated collection of machineverified program logics and compilers giving foundational correctness guarantees.par VeriStar ... entailment holds in a provedsound separation logic for C minor ... easily be ported to other separation logics...