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

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) 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

(10)

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

Describes a project that uses

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)