Forest automata for verification of heap manipulation

DOI10.1007/s10703-012-0150-8zbMath1284.68398OpenAlexW2065248162MaRDI QIDQ2441715

Jiří Šimáček, Tomáš Vojnar, Adam Rogalewicz, Peter Habermehl, Lukáš Holík

Publication date: 28 March 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-012-0150-8

zbMATH Keywords

tree automatashape analysispointersregular model checking

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items

Verification of heap manipulating programs with ordered data by extended forest automata, Counterexample Validation and Interpolation-Based Refinement for Forest Automata, Forest automata for verification of heap manipulation, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, Nested antichains for WS1S, Minimization of Visibly Pushdown Automata Using Partial Max-SAT, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Automated formal analysis and verification: an overview

Uses Software

• Predator
• HIP

Cites Work

• Unnamed Item
• Forest automata for verification of heap manipulation
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• Scalable Shape Analysis for Systems Code
• When Simulation Meets Antichains
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Compositional shape analysis by means of bi-abduction
• Decidable logics combining heap structures and data
• Shape Analysis for Composite Data Structures
• Automated Verification of Shape and Size Properties Via Separation Logic
• Computing Simulations over Tree Automata
• Programs with Lists Are Counter Automata
• Tools and Algorithms for the Construction and Analysis of Systems