Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
From MaRDI portal
Publication:3613378
DOI10.1007/11823230_5zbMath1225.68067MaRDI QIDQ3613378
Adam Rogalewicz, Ahmed Bouajjani, Peter Habermehl, Tomáš Vojnar
Publication date: 12 March 2009
Published in: Static Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11823230_5
68Q60: Specification and verification (program logics, model checking, etc.)
68P05: Data structures
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Handling Left-Quadratic Rules When Completing Tree Automata, Verifying Multithreaded Recursive Programs with Integer Variables, An Efficient Decision Procedure for Imperative Tree Data Structures, Computing Simulations over Tree Automata, Programs with lists are counter automata, Juggrnaut: using graph grammars for abstracting unbounded heap structures, Model checking dynamic memory allocation in operating systems, Automata-based verification of programs with tree updates, Equational approximations for tree automata completion, Approximated parameterized verification of infinite-state processes with global conditions, Verify heaps via unified model checking, Forest automata for verification of heap manipulation, A Game Theoretic Approach to the Analysis of Dynamic Networks, Automated formal analysis and verification: an overview, Counterexample Validation and Interpolation-Based Refinement for Forest Automata, Controlled Term Rewriting, A Logic-Based Framework for Reasoning about Composite Data Structures, Bottom-Up Shape Analysis, Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies, Monotonic Abstraction for Programs with Dynamic Memory Heaps, Abstracting Complex Data Structures by Hyperedge Replacement, Automata-Based Termination Proofs
Uses Software
