Verification of heap manipulating programs with ordered data by extended forest automata
From MaRDI portal
Publication:300414
DOI10.1007/s00236-015-0235-0zbMath1344.68136OpenAlexW2167064916MaRDI QIDQ300414
Bengt Jonsson, Parosh Aziz Abdulla, Lukáš Holík, Ondřej Lengál, Tomáš Vojnar, Cong Quy Trinh
Publication date: 28 June 2016
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00236-015-0235-0
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Programs with lists are counter automata
- Loop invariant synthesis in a combined abstract domain
- Forest automata for verification of heap manipulation
- Back to the future
- Relational inductive shape analysis
- Verifying Heap-Manipulating Programs in an SMT Framework
- Scalable Shape Analysis for Systems Code
- Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data
- Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata
- Automatic numeric abstractions for heap-manipulating programs
- Counterexample-guided focus
- An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Computer Aided Verification
- Computer Aided Verification
- A Reachability Predicate for Analyzing Low-Level Software
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Verification of heap manipulating programs with ordered data by extended forest automata
