Applying Predicates Abstraction on Trace Abstraction Refinement

Pongsak Suvanpong, Anthony Sloane and Franck Cassez
Macquarie University

Skink is a next generation software verification project at the Programming Language and Software verification group at Macquarie University. Skink verifies programs using traces. A trace is a path in the control flow graph of a program. Skink proves program correctness by checking traces that end at error locations are infeasible. Currently Skink uses trace abstraction refinement to check traces. In this talk, I will discuss about how trace abstraction refinement works and its limitations for proving traces with array and repeated locations. Then I will discuss our plan to apply predicates abstraction which is a technique for automatically inferring invariants to overcome the limitations.