On the almighty wand

DOI10.1016/J.IC.2011.12.003MaRDI QIDQ418137zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

complexityexpressive powerreasoning on linked listssatisfiabilitysecond-order logicseparation logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On the Almighty Wand
• Separation logic with one quantified variable
• Separation logic with one quantified variable
• Expressive completeness of separation logic with two variables and no separating conjunction
• Two-Variable Separation Logic and Its Inner Circle

Cites work

• Arithmetic Strengthening for Shape Analysis
• Beyond Shapes: Lists with Ordered Data
• BI as an assertion language for mutable data structures
• Context logic as modal logic, completeness and parametric inexpressivity
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Elimination of spatial connectives in static spatial logics
• Expressiveness and complexity of graph logic
• First-order logic with two variables and unary temporal logic
• Foundations of Software Science and Computation Structures
• 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
• scientific article; zbMATH DE number 1617328 (Why is no real title available?)
• scientific article; zbMATH DE number 2038747 (Why is no real title available?)
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• scientific article; zbMATH DE number 965572 (Why is no real title available?)
• Impossibility of an algorithm for the decision problem in finite classes
• Mechanizing Mathematical Reasoning
• Nondeterministic phase semantics and the undecidability of Boolean BI
• On the Almighty Wand
• Quantitative Separation Logic and Programs with Lists
• Reasoning about sequences of memory states
• Separating Graph Logic from MSO
• Static Analysis
• Static Analysis
• Tableaux and resource graphs for separation logic
• Tools and Algorithms for the Construction and Analysis of Systems
• Tractable Reasoning in a Fragment of Separation Logic
• Undecidability of propositional separation logic and its neighbours

Cited in

(39)

• Verify heaps via unified model checking
• Separation logic and logics with team semantics
• Prenex separation logic with one selector field
• Strong-separation logic
• Separation logic with one quantified variable
• A complete decision procedure for linearly compositional separation logic with data constraints
• A simple separation logic
• Two-Variable Separation Logic and Its Inner Circle
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Completeness for a first-order abstract separation logic
• Undecidability of propositional separation logic and its neighbours
• On the power of magic
• Automated theorem proving for assertions in separation logic with all connectives
• On the Almighty Wand
• Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
• Separation logics and modalities: a survey
• Separation logic with one quantified variable
• Trakhtenbrot’s Theorem in Coq
• On temporal and separation logics
• Extending propositional separation logic for robustness properties
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Tractability of separation logic with inductive definitions: beyond lists
• A complete axiomatisation for quantifier-free separation logic
• On the complexity of modal separation logics
• Expressive completeness of separation logic with two variables and no separating conjunction
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• Program Verification with Separation Logic
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• A Spatial Logic for Simplicial Models
• Sound Automation of Magic Wands
• The logic of separation logic: models and proofs
• Analysis of spatio-temporal properties of stochastic systems using TSTL
• Representation of Peano arithmetic in separation logic
• First-order hybrid separation logic
• Expressive completeness of separation logic in block-based cloud storage systems
• Expressiveness results for an inductive logic of separated relations
• Beyond symbolic heaps: deciding separation logic with inductive definitions
• Encoding Peano arithmetic in a minimal fragment of separation logic

Describes a project that uses

Uses Software

• TVLA

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)