We present several improvements to general-purpose sequential redundancy removal. First, we propose using a robust variety of synergistic transformation and verication algorithms to process the individual proof obligations. Experiments conrm that this more general approach enables greater speed and scalability, and identies a signicantly greater degree of redundancy, than previous approaches. Second, we demonstrate how we may generalize upon traditional redundancy removal applications and utilize the speculatively-reduced model to enhance bounded search, without needing to complete any proofs.

Access the entire document on the IBM Corp. website.