A logic of reachable patterns in linked data-structures

DOI10.1016/j.jlap.2006.12.001zbMath1121.03040arXiv0705.3610OpenAlexW1975156572MaRDI QIDQ2643337

Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Greta Yorsh, Ahmed Bouajjani

Publication date: 23 August 2007

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0705.3610

zbMATH Keywords

patternshape analysisprogram verificationweak monadic second-order logicdecidable logic with reachabilityheap-manipulating programsrouting expressiontransitive closure logics

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) 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

A Logic-Based Framework for Reasoning about Composite Data Structures ⋮ A logic of reachable patterns in linked data-structures ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Interactive and automated proofs for graph transformations ⋮ An Efficient Decision Procedure for Imperative Tree Data Structures

Uses Software

• JML
• MONA
• Timbuk
• TVLA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the undecidability of logics with converse, nominals, recursion and counting
• Undecidability results on two-variable logics
• Guarded fixed point logics and the monadic theory of countable trees.
• A logic of reachable patterns in linked data-structures
• Hybrid logics: characterization, interpolation and complexity
• Reachability Analysis of Term Rewriting Systems with Timbuk
• Easy problems for tree-decomposable graphs
• The monadic second-order logic of graphs, II: Infinite graphs of bounded width
• Graph minors. II. Algorithmic aspects of tree-width
• Languages that Capture Complexity Classes
• Recursive data structures
• On languages with two variables
• BI as an assertion language for mutable data structures
• Computer Science Logic
• Computer Aided Verification
• Computer Aided Verification
• Verifying properties of well-founded linked lists
• 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
• Foundations of Software Science and Computational Structures
• Verification, Model Checking, and Abstract Interpretation