Function Summarization Modulo Theories

DOI10.29007/d3btzbMath1415.68141OpenAlexW2900845427MaRDI QIDQ5222945

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

zbMATH Keywords

Craig interpolationsoftware verificationsatisfiability modulo theoriesbounded model checkingincremental verificationfunction summaries

Mathematics Subject Classification ID

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

Related Items (3)

SMT-based verification of program changes through summary repair ⋮ Unbounded procedure summaries from bounded environments ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

This page was built for publication: Function Summarization Modulo Theories