Introducing Abstractions via Rewriting
Mechanically assisted proofs of properties of a complex system require an accurate formal model of the system. If the model is too detailed the proof becomes intractible. 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. We have applied this technique to the Rockwell-Collins AAMP7 processor model and been able to improve significantly the analyzability of the model.
KeywordsOperational Semantic Assisted Proof Symbol Fix16 Abstraction Function Abstraction Approach
- 1.Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Kaufmann, M., Manolios, P., Moore, J. (eds.) Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, Boston (2000)Google Scholar
- 2.Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)Google Scholar