Abstract
We describe an algorithm for simplifying a class of symbolic expressions that arises in the symbolic execution of formal state machine models. These expressions are compositions of state access and change functions and if-then-else expressions, laced together with local variable bindings (e.g., lambda applications). The algorithm may be used in a stand-alone way, but is designed to be part of a larger system employing a mix of other strategies. The algorithm generalizes to a rewriting algorithm that can be characterized as outside-in or lazy, with respect both to variable instantiation and equality replacement. The algorithm exploits memoization or caching.
Keywords
Download to read the full chapter text
Chapter PDF
References
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.
M. Ayala-Ricon and Cesar Munoz. Explicit subsitutions and all that. Technical Report TR-2000-45, ICASE, NASA Langley Research Center, Hampton, Virginia, November 2000. http://www.icase.edu/Dienst/UI/2.0/Describe/ncstrl.icase/TR-2000-45.
W.R. Bevier, W.A. Hunt, J.S. Moore, and W.D. Young. Special issue on system verification. Journal of Automated Reasoning, 5(4):409–530, 1989.
R.S. Boyer and J.S. Moore. The sharing of structure in theorem-proving programs. In Machine Intelligence 7, pages 101–116. Edinburgh University Press, 1972.
R. S. Boyer and J.S. Moore. Single-threaded objects in ACL2. (submitted for publication), 1999.
Bishop Brock and Warren A. Hunt, Jr. Formally specifying and mechanically verifying programs for the Motorola complex arithmetic processor DSP. In 1997 IEEE International Conference on Computer Design, pages 31–36. IEEE Computer Society, October 1997.
N.G. de Bruijn. A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report TH-Report 78-WSK-03, Department of Mathematics, Technological University Eindhoven, Netherlands, 1978.
M. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
J. Grundy. Verified optimizations for the intel ia-64 architecture. In TPHOLs 2000, LNCS 1869, pages 215–232. Springer-Verlag, 2000.
J. Hickey and A. Nogin. Fast tactic-based theorem proving. In TPHOLs 2000, LNCS 1869, pages 252–267. Springer-Verlag, 2000.
W.A. Hunt and B. Brock. A formal HDL and its use in the FM9001 verification. Proceedings of the Royal Society, April 1992.
M. Kaufmann, P. Manolios, and J.S. Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, 2000.
M. Kaufmann, P. Manolios, and J.S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Press, 2000.
P. Manolios. Correctness of pipelined machines. In Formal Methods in Computer-Aided Design, FMCAD 2000, pages 161–178. Springer-Verlag LNCS 1954, 2000.
S.P. Miller and M. Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In Proceedings of WIFT’ 95: Workshop on Industrial-Strength Formal Specification Techniques, pages 2–16. IEEECS, April 1995.
J.S. Moore. Piton: A Mechanically Verified Assembly-Level Language. Automated Reasoning Series, Kluwer Academic Publishers, 1996.
S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), pages 748–752. Lecture Notes in Artificial Intelligence, Vol 607, Springer-Verlag, June 1992.
J. Sawada and W. Hunt. Processor verification with precise exceptions and speculative execution. In Computed Aided Verification, CAV’ 98, pages 135–146. Springer-Verlag LNCS 1427, 1998.
G. L. Steele, Jr. Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803, 1990.
Matthew Wilding, David Greve, and David Hardin. Efficient simulation of formal processor models. Formal Methods in System Design, to appear. Draft TR available as http://pobox.com/users/hokie/docs/efm.ps.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Strother Moore, J. (2001). Rewriting for Symbolic Execution of State Machine Models. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_41
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive