Automata-based verification of programs with tree updates

DOI10.1007/S00236-009-0108-5MaRDI QIDQ845236zbMATH OpenOpenAlexFDO

Authors Peter Habermehl, Radu Iosif, Tomáš Vojnar

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)

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Automata-based abstraction for automated verification of higher-order tree-processing programs
• Verifying higher-order functions with tree automata
• Certifying a Tree Automata Completion Checker
• Tree automata-based refinement with application to Horn clause verification
• Verification of tree-processing programs via higher-order model checking
• scientific article; zbMATH DE number 2040893
• Verification of concurrent programs: The automata-theoretic framework

Cites work

• scientific article; zbMATH DE number 4172381 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Automata, Languages and Programming
• Automated Verification of Shape and Size Properties Via Separation Logic
• Context logic as modal logic, completeness and parametric inexpressivity
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Static Analysis
• Tree Automata with Memory, Visibility and Structural Constraints
• Tree automata with one memory set constraints and cryptographic protocols
• Verifying Balanced Trees
• Visibly pushdown languages

Cited in

(9)

• Verification of heap manipulating programs with ordered data by extended forest automata
• Forest automata for verification of heap manipulation
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
• scientific article; zbMATH DE number 1629942 (Why is no real title available?)
• An efficient decision procedure for imperative tree data structures
• Computer Aided Verification
• Verification of heap manipulating programs with ordered data by extended forest automata
• Verifying Balanced Trees

Describes a project that uses

Uses Software

• TASC
• JML
• Spec#
• TestEra
• HIP

This page was built for publication: Automata-based verification of programs with tree updates

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q845236)