On the almighty wand

DOI10.1016/j.ic.2011.12.003zbMath1262.03051OpenAlexW2025750846MaRDI QIDQ418137

Rémi Brochenin, Etienne Lozes, Stéphane P. 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

complexitysecond-order logicsatisfiabilityexpressive powerseparation logicreasoning on linked lists

Mathematics Subject Classification ID

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

Related Items (23)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Program Verification with Separation Logic ⋮ Trakhtenbrot’s Theorem in Coq ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ Separation logic and logics with team semantics ⋮ Separation logic with one quantified variable ⋮ Separation logics and modalities: a survey ⋮ Two-Variable Separation Logic and Its Inner Circle ⋮ A Spatial Logic for Simplicial Models ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ Strong-separation logic ⋮ Verify heaps via unified model checking ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ On Temporal and Separation Logics ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ Unnamed Item ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Uses Software

• TVLA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about sequences of memory states
• Expressiveness and complexity of graph logic
• Elimination of spatial connectives in static spatial logics
• First-order logic with two variables and unary temporal logic
• 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
• Tableaux and Resource Graphs for Separation Logic
• On the Almighty Wand
• Quantitative Separation Logic and Programs with Lists
• Arithmetic Strengthening for Shape Analysis
• Separating Graph Logic from MSO
• Beyond Shapes: Lists with Ordered Data
• BI as an assertion language for mutable data 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
• Static Analysis
• Static Analysis
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Tools and Algorithms for the Construction and Analysis of Systems
• Mechanizing Mathematical Reasoning
• Impossibility of an algorithm for the decision problem in finite classes
• Foundations of Software Science and Computation Structures

This page was built for publication: On the almighty wand