A logic of reachable patterns in linked data-structures

DOI10.1016/j.jlap.2006.12.001zbMath1121.03040arXiv0705.3610MaRDI 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

pattern; shape analysis; program verification; weak monadic second-order logic; decidable logic with reachability; heap-manipulating programs; routing expression; transitive closure logics

Mathematics Subject Classification ID

03B70: Logic in computer science

03D05: Automata and formal grammars in connection with logical questions

68Q60: Specification and verification (program logics, model checking, etc.)

03B25: Decidability of theories and sets of sentences

68P05: Data structures

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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