Theory refinement for program verification

DOI10.1007/978-3-319-66263-3_22zbMATH Open1496.68191DBLPconf/sat/HyvarinenAMFCS17OpenAlexW2742433495WikidataQ57699293 ScholiaQ57699293MaRDI QIDQ1680264FDOQ1680264

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

Recommendations

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

Mathematics Subject Classification ID

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

Cited In (7)

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

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)