{"id":{"repo_id":"byu","oai_identifier":"oai:scholarsarchive.byu.edu:etd-1923"},"canonical_url":"https://search.dev.ndltd.org/etd/byu/oai:scholarsarchive.byu.edu:etd-1923","repository":{"repo_id":"byu","name":"Brigham Young University","base_url":"https://scholarsarchive.byu.edu/do/oai/"},"display":{"title":"Finding Termination and Time Improvement in Predicate Abstraction with Under-Approximation and Abstract Matching","abstract":"The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. The logic behind this approach is that if an error is found in the early coarse abstractions of the system, we save space and time. Our research improves AMCS by providing a refinement technique which guarantees termination. Our technique finds errors in less time and space by using an abstract state splitting algorithm based on intervals, which does not require a theorem prover.","abstract_html":"The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. The logic behind this approach is that if an error is found in the early coarse abstractions of the system, we save space and time. Our research improves AMCS by providing a refinement technique which guarantees termination. Our technique finds errors in less time and space by using an abstract state splitting algorithm based on intervals, which does not require a theorem prover.","abstract_has_math":false,"creators":["Kudra, Dritan"],"institution":"Brigham Young University - Provo","degree_name":"MS","degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T01:28:37Z","subjects":["software","computer","bugs","verification","validation","model checking","predicate abstraction","under approximation","bissimulation","precise abstraction","random DFS","MinOnly","pasareanu","abstract matching","dritan kudra","Computer Sciences"],"languages":["English"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://scholarsarchive.byu.edu/etd/924","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Kudra, Dritan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2007-06-11T07:00:00Z"]},{"key":"dc:publisher","label":"Institution","values":["Brigham Young University - Provo"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["MS"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["software","computer","bugs","verification","validation","model checking","predicate abstraction","under approximation","bissimulation","precise abstraction","random DFS","MinOnly","pasareanu","abstract matching","dritan kudra","Computer Sciences"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["English"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://scholarsarchive.byu.edu/etd/924","https://scholarsarchive.byu.edu/context/etd/article/1923/viewcontent/ETD_CISOPTR_1047.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Physical and Mathematical Sciences; Computer Science"]},{"key":"dc:description.abstract","label":"Abstract","values":["The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. The logic behind this approach is that if an error is found in the early coarse abstractions of the system, we save space and time. Our research improves AMCS by providing a refinement technique which guarantees termination. Our technique finds errors in less time and space by using an abstract state splitting algorithm based on intervals, which does not require a theorem prover."]},{"key":"dc:format","label":"Dc Format","values":["application:pdf"]},{"key":"dc:source","label":"Dc Source","values":["Brigham Young University - Provo"]},{"key":"dc:title","label":"Title","values":["Finding Termination and Time Improvement in Predicate Abstraction with Under-Approximation and Abstract Matching"]}]}],"canonical_facts":{"dc:creator":["Kudra, Dritan"],"dc:date":["2007-06-11T07:00:00Z"],"dc:description":["Physical and Mathematical Sciences; Computer Science"],"dc:description.abstract":["The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. The logic behind this approach is that if an error is found in the early coarse abstractions of the system, we save space and time. Our research improves AMCS by providing a refinement technique which guarantees termination. Our technique finds errors in less time and space by using an abstract state splitting algorithm based on intervals, which does not require a theorem prover."],"dc:format":["application:pdf"],"dc:identifier":["https://scholarsarchive.byu.edu/etd/924","https://scholarsarchive.byu.edu/context/etd/article/1923/viewcontent/ETD_CISOPTR_1047.pdf"],"dc:language":["English"],"dc:publisher":["Brigham Young University - Provo"],"dc:source":["Brigham Young University - Provo"],"dc:subject":["software","computer","bugs","verification","validation","model checking","predicate abstraction","under approximation","bissimulation","precise abstraction","random DFS","MinOnly","pasareanu","abstract matching","dritan kudra","Computer Sciences"],"dc:title":["Finding Termination and Time Improvement in Predicate Abstraction with Under-Approximation and Abstract Matching"],"dc:type":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T01:28:37Z"}