Design and evaluation of a formula cache for SMT-based bounded model checking tools
| dc.contributor.advisor | Fischer, Bernd | en_ZA |
| dc.contributor.author | Breytenbach, Jean Anré | en_ZA |
| dc.contributor.other | Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences (Computer Science) | en_ZA |
| dc.date.accessioned | 2018-02-28T09:20:37Z | |
| dc.date.accessioned | 2018-04-09T07:10:07Z | |
| dc.date.available | 2018-02-28T09:20:37Z | |
| dc.date.available | 2018-04-09T07:10:07Z | |
| dc.date.issued | 2018-03 | |
| dc.description | Thesis (MSc)--Stellenbosch University, 2018. | en_ZA |
| dc.description.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. | en_ZA |
| dc.description.abstract | 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. | af_ZA |
| dc.description.abstract | rs201805 | |
| dc.format.extent | xviii, 137 pages : colour illustrations | en_ZA |
| dc.identifier.uri | http://hdl.handle.net/10019.1/103809 | |
| dc.language.iso | en_ZA | en_ZA |
| dc.publisher | Stellenbosch : Stellenbosch University | en_ZA |
| dc.rights.holder | Stellenbosch University | en_ZA |
| dc.subject | Bounded model checking | en_ZA |
| dc.subject | UCTD | en_ZA |
| dc.subject | Model checking (Computer science) | en_ZA |
| dc.subject | Satisfiability modulo theories (SMT) | en_ZA |
| dc.subject | Computer software -- Verification | en_ZA |
| dc.subject | Integrated circuits -- Verification | en_ZA |
| dc.title | Design and evaluation of a formula cache for SMT-based bounded model checking tools | en_ZA |
| dc.type | Thesis | en_ZA |