-
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 separation-logic-based 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 Small-Step cminor. cminor is a mid-level 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 large-scale machine ... checked proof of a Separation Logic w.r.t. a small-step semantics. The work presented...
-
Slide
- Referenced in 20 articles
[sw28542]
- SLIDE - Separation Logic with Inductive Definitions. Automata-based entailment checking for Separation Logic with Inductive ... prototype tool for checking entailment in Separation Logic with user-provided 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 higher-order list predicates, but they...
-
Charge!
- Referenced in 10 articles
[sw22731]
- Charge! A framework for higher-order separation logic in Coq. We present a comprehensive ... shallow embedding of a higher-order separation logic for a subset of Java ... abstraction similar to pen-and-paper separation-logic 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...
-
SOLA-VOF
- 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, three-valued logic, eager minimization, BDD-based 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 separation-logic based correctness...
-
VerCors
- Referenced in 7 articles
[sw11259]
- VerCors project we use permission-based 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 permission-based separation logic is suitable to verify functional correctness properties...
-
Viper
- Referenced in 9 articles
[sw15038]
- verification techniques based on first-order 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 first-order 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 ... large-scale program development, allowing modularity, separate compilation, and numerous optimization/time trade-offs...