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)

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

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)