Reasoning about Programs-rnechamcul wv-zfzcatton General Terms Verification

We descrlbc a method for u smg abstraction to reduce the complexity of temporal-loglc model checking Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever exammmg the corresponding ’ unabstracted model. We show how this abstract model can be used to verify properties of the orgmal program. We have Implemented a system based on these tecbmques, and we demonstrate them practlcabty using a number of examples, including a program representing a pipelined ALU circuit with over 10 lJ”0 states