Finding Termination and Time Improvement in Predicate Abstraction with Under-Approximation and Abstract Matching

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.

Name thesis:degree_name

MS

Grantor dc:publisher

Brigham Young University - Provo

Author dc:creator

• Kudra, Dritan

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

Language dc:language

English

Repository record dc:identifier

https://scholarsarchive.byu.edu/etd/924

OAI identifier oai:identifier

oai:scholarsarchive.byu.edu:etd-1923