Optimizing Slicing of Formal Specifications by Deductive Verification

Slicing is a technique for extracting parts of programs or specifications with respect to certain criteria of interest. The extraction is carried out in such a way that properties as described by the slicing criterion are preserved, i.e., they hold in the complete program if and only if they hold in the sliced program. In verification, slicing is often employed to reduce the state space of specifications to a size tractable by a model checker. The computation of specification slices relies on the construction of dependence graphs, reflecting (at least) control and data dependencies in specifications. The more dependencies the graph has, the less removal of parts is possible. In this paper we present a technique for optimizing the construction of the dependence graph by using deductive verification techniques. More precisely, we propose a technique for showing that certain control dependencies in the graph can be eliminated. The technique employs small deductive proofs of the enablednes...

• Type: Journal
• Year: 2006
• Where: NJC
• Authors: Ingo Brückner, Björn Metzler, Heike Wehrheim
• Keywords: Dependence Graphs, NJC 2006, Specification Slices, Specifications