Abstraction refinement with Craig interpolation and symbolic pushdown systems

MaRDI QIDQ3620428zbMATH OpenFDO

Authors Javier Esparza, Stefan Kiefer, Stefan Schwoon

Publication date 14 April 2009

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)

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

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

Describes a project that uses

Uses Software

• MOPED
• jMoped

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)