Automata-based verification of programs with tree updates

DOI10.1007/s00236-009-0108-5zbMath1185.68414OpenAlexW1604924060MaRDI QIDQ845236

Peter Habermehl, Tomáš Vojnar, Radu Iosif

Publication date: 5 February 2010

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-009-0108-5

Mathematics Subject Classification ID

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

Related Items

An Efficient Decision Procedure for Imperative Tree Data Structures

Uses Software

• TASC
• JML
• Spec#
• TestEra
• HIP

Cites Work

• Tree automata with one memory set constraints and cryptographic protocols
• Context logic as modal logic
• Visibly pushdown languages
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Verifying Balanced Trees
• Automated Verification of Shape and Size Properties Via Separation Logic
• Automata, Languages and Programming
• Static Analysis
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Tree Automata with Memory, Visibility and Structural Constraints
• Unnamed Item
• Unnamed Item