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

complexitysatisfiabilityseparation logicsecond-order logicexpressive powerreasoning on linked lists

Mathematics Subject Classification ID

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)

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

• 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?)
• Arithmetic Strengthening for Shape Analysis
• BI as an assertion language for mutable data structures
• Beyond Shapes: Lists with Ordered Data
• 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
• 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
• First-order logic with two variables and unary temporal logic
• Foundations of Software Science and Computation Structures
• 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

(33)

• Verify heaps via unified model checking
• Automated theorem proving for assertions in separation logic with all connectives
• On the complexity of modal separation logics
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Separation logics and modalities: a survey
• Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
• A complete axiomatisation for quantifier-free separation logic
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• 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
• Separation logic and logics with team semantics
• On temporal and separation logics
• Analysis of spatio-temporal properties of stochastic systems using TSTL
• scientific article; zbMATH DE number 7561347 (Why is no real title available?)
• Expressive completeness of separation logic with two variables and no separating conjunction
• Undecidability of propositional separation logic and its neighbours
• Program Verification with Separation Logic
• Two-Variable Separation Logic and Its Inner Circle
• Tractability of separation logic with inductive definitions: beyond lists
• A simple separation logic
• Trakhtenbrot’s Theorem in Coq
• An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
• 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
• The logic of separation logic: models and proofs
• A Spatial Logic for Simplicial Models

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)