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

VeriFast
 Referenced in 54 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 23 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 32 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 19 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...

Charge!
 Referenced in 9 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 42 articles
[sw08981]
 combine the currently separated research efforts of the functional and logic programming communities...

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

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

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

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

VeriSmall
 Referenced in 6 articles
[sw09788]
 with respect to our Separation Logic for C minor; this in turn is proved correct...

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