Counterexample validation and interpolation-based refinement for forest automata
DOI10.1007/978-3-319-52234-0_16zbMATH Open1484.68103OpenAlexW2570552138MaRDI QIDQ2961572FDOQ2961572
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
Recommendations
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Interpolation and SAT-based model checking.
- Automatic numeric abstractions for heap-manipulating programs
- Lazy Abstraction with Interpolants
- Loop invariant synthesis in a combined abstract domain
- Forest automata for verification of heap manipulation
- Abstract regular tree model checking
- Verification of heap manipulating programs with ordered data by extended forest automata
- Scalable Shape Analysis for Systems Code
- Accurate invariant checking for programs manipulating lists and arrays with infinite data
- Counterexample-guided focus
- Programs with lists are counter automata
- Computer Aided Verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- Tools and Algorithms for the Construction and Analysis of Systems
- Spatial interpolants
- Counterexample validation and interpolation-based refinement for forest automata
Cited In (2)
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)