Design and evaluation of a formula cache for SMT-based bounded model checking tools
Date
2018-03
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
ENGLISH ABSTRACT : Program verification is a computationally expensive and time-consuming process.
Bounded model checking is a branch of program verification that produces FOL formulas
to be checked for satisfiability by an SMT solver. These formulas encode state
transitions to states where property violations will occur and the SMT solver attempts
to find a list of variable assignments that would create a path to one of these states.
Bounded model checking tools create these formulas by iteratively increasing an unwind
bound k that dictates the number of transitions that can be present in a path, for
each unwind bound k all possible paths of length k are generated. Any state containing
a property violation that is generated during the unwind bound k − 1 should also be
present during the unwind bound k with perhaps a longer path to reach it.
This creates many of the same paths being checked during each subsequent iteration
causing the SMT solver to potentially perform duplicate work. This thesis seeks to
build and evaluate a formula cache in which to store parts of the formula for which the
satisfiability is already known. During subsequent iterations the formula can be sliced
by removing the parts that are found in the cache, providing smaller formulas for the
SMT solver which should take less time to solve. Similar formula caches have already
proven successful in the field of symbolic execution.
Multiple techniques are described to modify the formulas to increase the likelihood
of finding a match in the cache and these techniques are combined in a multitude of
ways to generate a collection of caching strategies. These strategies are then evaluated
against multiple data sets to find the best performing strategies and to identify the types
of problems that benefit the most from caching. The results are then compared to the
results of caching formulas during symbolic execution to gain insight as to how these
different approaches effectively implement caching.
AFRIKAANSE OPSOMMING : Program verifikasie is ’n duur en tydrowende berekeningsproses. Begrensde modeltoetsing is ’n tak van program verifikasie wat FOL-formules genereer en toets vir voldoening deur gebruik te maak van ’n SMT oplosser. Hierdie formules koordineer die ¨ paaie deur programme waar eienskappe hul waardes verkry buite die bepaalde spesi- fikasies. Begrensde modeltoetsing gereedskap bou hierdie formules deur iteratief ’n bogrenswaardewaarde k, wat die aantal stappe wat in ’n pad teenwoordig kan wees, te verhoog. Vir elke bogrenswwaarde k word alle moontlike paaie van lengte k gegenereer. Indien ’n formule op ’n sekere pad nie voldoen aan die spesifikasie vir k −1 stappe nie, sal daardie gedeelte van die formule nogsteeds ongeldig wees vir k stappe. Dus word baie van dieselfde paaie tydens elke opeenvolgende iterasie gegenereer. Gevolglik word baie van die werk gedupliseer vir die SMT oplosser tydens opeenvolgende iterasies. Hierdie tesis poog om ’n formulekas te bou en te evalueer, wat dele van die formule op kyk waarvoor die voldoening reeds bekend is. Tydens opeenvolgende iterasies kan die formule gesny word deur van die gedeeltes te verwyder wat in die formulekas gevind kan word. Soortgelyke formulekasstelsels is reeds suksesvol bewys in die gebied van simboliese uitvoering. ’n Aantal tegnieke word beskryf om die formules te verander gedurende die opkyk proses. Daar word verwag dat die transformasies die waarskynlikheid om ’n ekwivalente formule in die formulekas te vind, sal verhoog. Die tegnieke word gekombineer in veelvuldige strategiee om dan te evalueer watter kombinasies die beste resultate lewer ¨ vir begrensde modeltoetsing.
rs201805
AFRIKAANSE OPSOMMING : Program verifikasie is ’n duur en tydrowende berekeningsproses. Begrensde modeltoetsing is ’n tak van program verifikasie wat FOL-formules genereer en toets vir voldoening deur gebruik te maak van ’n SMT oplosser. Hierdie formules koordineer die ¨ paaie deur programme waar eienskappe hul waardes verkry buite die bepaalde spesi- fikasies. Begrensde modeltoetsing gereedskap bou hierdie formules deur iteratief ’n bogrenswaardewaarde k, wat die aantal stappe wat in ’n pad teenwoordig kan wees, te verhoog. Vir elke bogrenswwaarde k word alle moontlike paaie van lengte k gegenereer. Indien ’n formule op ’n sekere pad nie voldoen aan die spesifikasie vir k −1 stappe nie, sal daardie gedeelte van die formule nogsteeds ongeldig wees vir k stappe. Dus word baie van dieselfde paaie tydens elke opeenvolgende iterasie gegenereer. Gevolglik word baie van die werk gedupliseer vir die SMT oplosser tydens opeenvolgende iterasies. Hierdie tesis poog om ’n formulekas te bou en te evalueer, wat dele van die formule op kyk waarvoor die voldoening reeds bekend is. Tydens opeenvolgende iterasies kan die formule gesny word deur van die gedeeltes te verwyder wat in die formulekas gevind kan word. Soortgelyke formulekasstelsels is reeds suksesvol bewys in die gebied van simboliese uitvoering. ’n Aantal tegnieke word beskryf om die formules te verander gedurende die opkyk proses. Daar word verwag dat die transformasies die waarskynlikheid om ’n ekwivalente formule in die formulekas te vind, sal verhoog. Die tegnieke word gekombineer in veelvuldige strategiee om dan te evalueer watter kombinasies die beste resultate lewer ¨ vir begrensde modeltoetsing.
rs201805
Description
Thesis (MSc)--Stellenbosch University, 2018.
Keywords
Bounded model checking, UCTD, Model checking (Computer science), Satisfiability modulo theories (SMT), Computer software -- Verification, Integrated circuits -- Verification