Path predicate abstraction by complete interval property checking

This paper describes a method to create an abstract model from a set of properties fulfilling a certain completeness criterion. The proposed abstraction can be understood as a path predicate abstraction. As in predicate abstraction, certain concrete states (called important states) are abstracted by predicates on the state variables. Additionally, paths between important states are abstracted by path predicates that trigger single transitions in the abstract model. As results, the non-important states are abstracted away and the abstract model becomes time-abstract as it is no longer cycle-accurate. Transitions in the abstract model represent finite sequences of transitions in the concrete model. In order to make this abstraction sound for proving liveness and safety properties it is necessary to put certain restrictions on the choice of state predicates. We show that Complete Interval Property Checking (C-IPC) can be used to create such an abstraction. Our experimental results include an industrial case study and demonstrate that our method can prove global system properties which are beyond the scope of conventional model checking.