Show simple item record

Software Model Checking with Uninterpreted Functions

dc.contributor.authorBueno, Denis
dc.date.accessioned2021-06-08T23:16:01Z
dc.date.available2021-06-08T23:16:01Z
dc.date.issued2021
dc.date.submitted2021
dc.identifier.urihttps://hdl.handle.net/2027.42/168092
dc.description.abstractSoftware model checkers attempt to algorithmically synthesize an inductive proof that a piece of software is safe. Such proofs are composed of complex logical assertions about program variables and control structures, and are computationally expensive to produce. Our unifying motivation is to increase the efficiency of verifying software control behavior despite its dependency on data. Control properties include important topics such as mutual exclusion, safe privilege elevation, and proper usage of networking and other APIs. These concerns motivate our techniques and evaluations. Our approach integrates an efficient abstraction procedure based on the logic of equality with uninterpreted functions (EUF) into the core of a modern model checker. Our checker, called euforia, targets control properties by treating a program's data operations and relations as uninterpreted functions and predicates, respectively. This reduces the cost of building inductive proofs, especially for verifying control relationships in the presence of complex but irrelevant data processing. We show that our method is sound and terminates. We provide a ground-up implementation and evaluate the abstraction on a variety of software verification benchmarks. We show how to extend this abstraction to memory-manipulating programs. By judicious abstraction of array operations to EUF, we show that we can directly reason about array reads and adaptively learn lemmas about array writes leading to significant performance improvements over existing approaches. We show that our abstraction of array operations completely eliminates much of the array theory reasoning otherwise required. We report on experiments with and without abstraction and compare our checker to the state of the art. Programs with procedures pose unique difficulties and opportunities. We show how to retrofit a model checker not supporting procedures so that it supports modular analysis of programs with non-recursive procedures. This technique applies to euforia as well as other logic-based algorithms. We show that this technique enables logical assertions about procedure bodies to be reused at different call sites. We report on experiments on software benchmarks compared to the alternative of inlining all procedures.
dc.language.isoen_US
dc.subjectSoftware model checking
dc.subjectEquality with uninterpreted functions
dc.titleSoftware Model Checking with Uninterpreted Functions
dc.typeThesis
dc.description.thesisdegreenamePHD
dc.description.thesisdegreedisciplineComputer Science & Engineering
dc.description.thesisdegreegrantorUniversity of Michigan, Horace H. Rackham School of Graduate Studies
dc.contributor.committeememberSakallah, Karem A
dc.contributor.committeememberLafortune, Stephane
dc.contributor.committeememberGurfinkel, Arie
dc.contributor.committeememberWeimer, Westley R
dc.subject.hlbsecondlevelComputer Science
dc.subject.hlbtoplevelEngineering
dc.description.bitstreamurlhttp://deepblue.lib.umich.edu/bitstream/2027.42/168092/1/dlbueno_1.pdf
dc.identifier.doihttps://dx.doi.org/10.7302/1519
dc.identifier.orcid0000-0001-6944-5022
dc.identifier.name-orcidBueno, Denis; 0000-0001-6944-5022en_US
dc.working.doi10.7302/1519en
dc.owningcollnameDissertations and Theses (Ph.D. and Master's)


Files in this item

Show simple item record

Accessibility: If you are unable to use this file in its current format, please select the Contact Us link and we can modify it to make it more accessible to you.