Introducing Abstractions via Rewriting

  • William D. Young
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


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.


Operational Semantic Assisted Proof Symbol Fix16 Abstraction Function Abstraction Approach 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 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. 2.
    Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)Google Scholar
  3. 3.
    Wilding, M., Greve, D., Hardin, D.: Efficient simulation of formal processor models. Formal Methods in System Design 18(3), 233–248 (2001)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • William D. Young
    • 1
  1. 1.Department of Computer SciencesThe University of Texas at Austin 

Personalised recommendations