On the almighty wand

DOI10.1016/J.IC.2011.12.003MaRDI QIDQ418137zbMATHOpenAlexFDO

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)

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