Function summarization modulo theories

DOI10.29007/D3BTMaRDI QIDQ5222945zbMATH OpenOpenAlexFDO

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

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

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)

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

Cited in

(7)

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

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)