Theory refinement for program verification

DOI10.1007/978-3-319-66263-3_22MaRDI QIDQ1680264zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Antti E. J. Hyvärinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina

Publication date 15 November 2017

Full work available at URL https://kclpure.kcl.ac.uk/portal/en/publications/theory-refinement-for-program-verification(f9107970-6b01-4d40-afcb-bc92984e606a).html

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Function summarization modulo theories
• Refinement for structured concurrent programs
• Artificial Intelligence and Symbolic Computation
• scientific article; zbMATH DE number 1953015
• Reachability modulo theories

Cited in

(7)

• Lattice-based refinement in bounded model checking
• Reachability modulo theories
• Function summarization modulo theories
• Automated verification and refinement for physical-layer protocols
• Integrated Formal Methods
• Embedded domain specific verifiers
• Constraint reusing and k-induction for three-valued bounded model checking

This page was built for publication: Theory refinement for program verification

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