Function summarization modulo theories

DOI10.29007/D3BTzbMATH Open1415.68141OpenAlexW2900845427MaRDI QIDQ5222945FDOQ5222945

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

Publication date: 4 July 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.29007/d3bt

Recommendations

• Theory refinement for program verification
• Unbounded procedure summaries from bounded environments
• SMT-based model checking for recursive programs
• Back to the future, revisiting precise program verification using SMT solvers
• A unifying view on SMT-based software verification

zbMATH Keywords

satisfiability modulo theoriesCraig interpolationbounded model checkingsoftware verificationincremental verificationfunction summaries

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (5)

• Unbounded procedure summaries from bounded environments
• SMT-based verification of program changes through summary repair
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Formula normalizations in verification
• Transition power abstractions for deep counterexample detection

This page was built for publication: Function summarization modulo theories

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