Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Design and evaluation of a formula cache for SMT-based bounded model checking tools
Thesis (MSc)--Stellenbosch University, 2018.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2018
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613914649329664 |
|---|---|
| access_status_str | Open Access |
| author | Breytenbach, Jean Anré |
| author2 | Fischer, Bernd |
| author_browse | Breytenbach, Jean Anré Fischer, Bernd |
| author_facet | Fischer, Bernd Breytenbach, Jean Anré |
| author_sort | Breytenbach, Jean Anré |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (MSc)--Stellenbosch University, 2018. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/103809 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:43:43.080Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2018 |
| publishDateRange | 2018 |
| publishDateSort | 2018 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/103809 Design and evaluation of a formula cache for SMT-based bounded model checking tools Breytenbach, Jean Anré Fischer, Bernd Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences (Computer Science) Bounded model checking UCTD Model checking (Computer science) Satisfiability modulo theories (SMT) Computer software -- Verification Integrated circuits -- Verification Thesis (MSc)--Stellenbosch University, 2018. 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 2018-02-28T09:20:37Z 2018-04-09T07:10:07Z 2018-02-28T09:20:37Z 2018-04-09T07:10:07Z 2018-03 Thesis http://hdl.handle.net/10019.1/103809 en_ZA Stellenbosch University xviii, 137 pages : colour illustrations application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Bounded model checking UCTD Model checking (Computer science) Satisfiability modulo theories (SMT) Computer software -- Verification Integrated circuits -- Verification Breytenbach, Jean Anré Design and evaluation of a formula cache for SMT-based bounded model checking tools |
| title | Design and evaluation of a formula cache for SMT-based bounded model checking tools |
| title_full | Design and evaluation of a formula cache for SMT-based bounded model checking tools |
| title_fullStr | Design and evaluation of a formula cache for SMT-based bounded model checking tools |
| title_full_unstemmed | Design and evaluation of a formula cache for SMT-based bounded model checking tools |
| title_short | Design and evaluation of a formula cache for SMT-based bounded model checking tools |
| title_sort | design and evaluation of a formula cache for smt based bounded model checking tools |
| topic | Bounded model checking UCTD Model checking (Computer science) Satisfiability modulo theories (SMT) Computer software -- Verification Integrated circuits -- Verification |
| url | http://hdl.handle.net/10019.1/103809 |
| work_keys_str_mv | AT breytenbachjeananre designandevaluationofaformulacacheforsmtbasedboundedmodelcheckingtools |