Counterexample validation and interpolation-based refinement for forest automata

DOI10.1007/978-3-319-52234-0_16MaRDI QIDQ2961572zbMATH OpenOpenAlexFDO

Authors Lukáš Holik, Martin Hruška, Ondřej Lengál, Adam Rogalewicz, Tomáš Vojnar

Publication date 21 February 2017

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-52234-0_16

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
• Refinement of Trace Abstraction
• scientific article; zbMATH DE number 1670775
• Thread-modular counterexample-guided abstraction refinement
• Abstraction refinement with Craig interpolation and symbolic pushdown systems

Cites work

• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Abstract regular tree model checking
• Accurate invariant checking for programs manipulating lists and arrays with infinite data
• Automatic numeric abstractions for heap-manipulating programs
• Computer Aided Verification
• Counterexample validation and interpolation-based refinement for forest automata
• Counterexample-guided focus
• Forest automata for verification of heap manipulation
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Loop invariant synthesis in a combined abstract domain
• Programs with lists are counter automata
• Scalable Shape Analysis for Systems Code
• Spatial interpolants
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of heap manipulating programs with ordered data by extended forest automata

Cited in

(2)

• Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
• Counterexample validation and interpolation-based refinement for forest automata

This page was built for publication: Counterexample validation and interpolation-based refinement for forest automata

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