Sciweavers

Share
NJC
2006

Optimizing Slicing of Formal Specifications by Deductive Verification

10 years 1 months ago
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...
Ingo Brückner, Björn Metzler, Heike Wehr
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2006
Where NJC
Authors Ingo Brückner, Björn Metzler, Heike Wehrheim
Comments (0)
books