Refinement of Trace Abstraction
From MaRDI portal
Publication:3392921
DOI10.1007/978-3-642-03237-0_7zbMath1248.68146OpenAlexW1841626152MaRDI QIDQ3392921
Andreas Podelski, Jochen Hoenicke, Matthias Heizmann
Publication date: 18 August 2009
Published in: Static Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-03237-0_7
Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (12)
A tree-based approach to data flow proofs ⋮ Loop verification with invariants and contracts ⋮ Verifying the correctness of distributed systems via mergeable parallelism ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ A unifying view on SMT-based software verification ⋮ Unbounded procedure summaries from bounded environments ⋮ Tree dimension in verification of constrained Horn clauses ⋮ Horn clause verification with convex polyhedral abstraction and tree automata-based refinement ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ Automated Program Verification ⋮ Proving Safety with Trace Automata and Bounded Model Checking ⋮ Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Abstractions from proofs
- Slicing Abstractions
- Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
- Lazy abstraction
- Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Automatically Refining Abstract Interpretations
- Lazy Abstraction with Interpolants
- Static Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
This page was built for publication: Refinement of Trace Abstraction
