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.
College and Department
Physical and Mathematical Sciences; Computer Science
BYU ScholarsArchive Citation
Kudra, Dritan, "Finding Termination and Time Improvement in Predicate Abstraction with Under-Approximation and Abstract Matching" (2007). Theses and Dissertations. 924.
software, computer, bugs, verification, validation, model checking, predicate abstraction, under approximation, bissimulation, precise abstraction, random DFS, MinOnly, pasareanu, abstract matching, dritan kudra