Abstraction refinement with Craig interpolation and symbolic pushdown systems

zbMATH Open1172.68541MaRDI QIDQ3620428FDOQ3620428

Authors: Javier Esparza, Stefan Kiefer, Stefan Schwoon 

Publication date: 14 April 2009

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Guiding Craig interpolation with domain-specific abstractions
• Abstractions from proofs
• Lazy Abstraction with Interpolants
• scientific article; zbMATH DE number 1670775

zbMATH Keywords

model-checking

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (9)

• Counterexample validation and interpolation-based refinement for forest automata
• Guiding Craig interpolation with domain-specific abstractions
• Lazy Abstraction with Interpolants
• Faster pushdown reachability analysis with applications in network verification
• Refinement of Trace Abstraction
• Boosting Lazy Abstraction for SystemC with Partial Order Reduction
• An automated quantitative information flow analysis for concurrent programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Abstractions from proofs

Uses Software

• jMoped
• MOPED

This page was built for publication: Abstraction refinement with Craig interpolation and symbolic pushdown systems

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