- Referenced in 51 articles
- 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...
- Referenced in 64 articles
- 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...
- Referenced in 289 articles
- beginning of logic programming, but it became prominent as a separate area around 1977 when...
- Referenced in 29 articles
- 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...
- Referenced in 19 articles
- 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...
- Referenced in 20 articles
- 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...
- Referenced in 32 articles
- symbolic execution and abstraction using separation logic. The proposed technology has been implemented...
- Referenced in 25 articles
- construction. The core simulation routines are logically separated from the model building interface and written...
- Referenced in 21 articles
- algorithms have been integrated, focusing on Separation Logic with inductively defined predicates. For information...
- Referenced in 18 articles
- were originally inspired by works on separation logic with higher-order list predicates, but they...
- Referenced in 10 articles
- 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...
- Referenced in 45 articles
- combine the currently separated research efforts of the functional and logic programming communities...
- Referenced in 86 articles
- intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally...
- Referenced in 44 articles
- 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...
- Referenced in 133 articles
- 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...
- Referenced in 7 articles
- Separation Logic Framework for Imperative HOL. We provide a framework for separation-logic based correctness...
- Referenced in 7 articles
- 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...
- Referenced in 9 articles
- 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...
- Referenced in 6 articles
- properties. The logic supports mixing of separation logic and first-order logic assertions, yielding expressive...
- Referenced in 69 articles
- 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...