Property dependent abstraction of control structure for software verification

Abstract

In this paper we present a technique to compute abstract models for formal system verification. The method reduces the state space by eliminating those parts of a system model which are not required to check a property. The abstract model depends on the property, which is a formula of the next-less fragment of CTL∗. The algorithm reads a system description, annotates it with abstract sub-models for the statements, which are finally composed as abstract model for the system. In the paper we introduce the core algorithm and illustrate it by an example.