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.

Degree

MS

College and Department

Physical and Mathematical Sciences; Computer Science

Rights

http://lib.byu.edu/about/copyright/

Date Submitted

2007-06-11

Document Type

Thesis

Handle

http://hdl.lib.byu.edu/1877/etd1875

Keywords

software, computer, bugs, verification, validation, model checking, predicate abstraction, under approximation, bissimulation, precise abstraction, random DFS, MinOnly, pasareanu, abstract matching, dritan kudra

Language

English

Download

Share

COinS