On the almighty wand
DOI10.1016/J.IC.2011.12.003zbMATH Open1262.03051OpenAlexW2025750846MaRDI QIDQ418137FDOQ418137
Authors: Rémi Brochenin, Etienne Lozes, Stéphane Demri 
Publication date: 24 May 2012
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2011.12.003
Recommendations
Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)
Cites Work
- Title not available (Why is that?)
- BI as an assertion language for mutable data structures
- Title not available (Why is that?)
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Title not available (Why is that?)
- Arithmetic Strengthening for Shape Analysis
- Tableaux and resource graphs for separation logic
- First-order logic with two variables and unary temporal logic
- Mechanizing Mathematical Reasoning
- Elimination of spatial connectives in static spatial logics
- Nondeterministic phase semantics and the undecidability of Boolean BI
- Tractable Reasoning in a Fragment of Separation Logic
- Undecidability of propositional separation logic and its neighbours
- Context logic as modal logic, completeness and parametric inexpressivity
- On the Almighty Wand
- Quantitative Separation Logic and Programs with Lists
- Separating Graph Logic from MSO
- Beyond Shapes: Lists with Ordered Data
- Title not available (Why is that?)
- Title not available (Why is that?)
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Static Analysis
- Static Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Impossibility of an algorithm for the decision problem in finite classes
- Foundations of Software Science and Computation Structures
- Reasoning about sequences of memory states
- Expressiveness and complexity of graph logic
Cited In (33)
- Automated theorem proving for assertions in separation logic with all connectives
- Verify heaps via unified model checking
- On the complexity of modal separation logics
- Title not available (Why is that?)
- Separation logics and modalities: a survey
- Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Separation logic with one quantified variable
- On the power of magic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- On temporal and separation logics
- Separation logic and logics with team semantics
- Analysis of spatio-temporal properties of stochastic systems using TSTL
- Title not available (Why is that?)
- Expressive completeness of separation logic with two variables and no separating conjunction
- Program Verification with Separation Logic
- Undecidability of propositional separation logic and its neighbours
- Two-Variable Separation Logic and Its Inner Circle
- Tractability of separation logic with inductive definitions: beyond lists
- Trakhtenbrot’s Theorem in Coq
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- A simple separation logic
- Sound Automation of Magic Wands
- Prenex separation logic with one selector field
- Separation logic with one quantified variable
- A complete decision procedure for linearly compositional separation logic with data constraints
- Completeness for a first-order abstract separation logic
- Strong-separation logic
- On the Almighty Wand
- Title not available (Why is that?)
- The logic of separation logic: models and proofs
- A Spatial Logic for Simplicial Models
Uses Software
This page was built for publication: On the almighty wand
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q418137)
