Date: Tue, 17 May 2005 14:42:01 -0500 (CDT) Subject: ACL2 this week We'll be meeting this week at the usual time and place. I will be speaking about the following. --Bill Young ABSTRACT: Mechanically assisted proof of properties of a complex system requires an accurate formal model of the system. If the model is too detailed the proof becomes intractible. Automated reasoning tools can provide invaluable assistance in managing such a complex proof, but typically still require that the human user have a deep and detailed insight into the system being verified. We outline techniques for automatically ``retrofitting'' a detailed low-level model with abstractions that facilitate reasoning about the properties of a model. The abstractions are introduced through semantics-preserving rewrite rules that guarantee that the resulting abstract model describes the system as faithfully and precisely as the original low-level model. We have applied this technique to the Rockwell-Collins AAMP7 processor model and been able to improve significantly the analyzability of the model. We used the ACL2 theorem proving system to manage the process, the ACL2 rewriter to replace complex terms by more abstract versions, and the prover to assure that the process preserves semantic equivalence.