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

Related Items (5)

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

This page was built for publication: A logic of reachable patterns in linked data-structures