Abstract
Forte is a formal verification system developed by Intel’s Strategic CAD Labs for applications in hardware design and verification. Forte integrates model checking and theorem proving within a functional programming language, which both serves as an extensible specification language and allows the system to be scripted and customized. The latest version of this language, called reFL ect, has quotation and antiquotation constructs that build and decompose expressions in the language itself. This provides combination of pattern-matching and reflection features tailored especially for the Forte approach to verification. This short paper is an abstract of an invited presentation given at the International Conference on Integrated Formal Methods in 2004, in which the philosophy and architecture of the Forte system are described and an account is given of the role of reFL ect in the system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Lifted-fl: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 23–340. Springer, Heidelberg (1999)
Barras, B.: Proving and Computing in HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 17–37. Springer, Heidelberg (2000)
Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 24–40. Springer, Heidelberg (2002)
Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: Hardware design in Haskell. In: Functional Programming: International Conference, ICFP 1998, pp. 174–184. ACM Press, New York (1998)
Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5, 56–68 (1940)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
Grundy, J., Melham, T., O’Leary, J.: A Reflective Functional Language for Hardware Design and Theorem Proving, Research Report PRG-RR-03-16, Programming Research Group, Oxford University (October 2003)
Harper, R., MacQueen, D., Milner, R.: Standard ML, Report 86-2, University of Edinburgh, Laboratory for Foundations of Computer Science (1986)
Harrison, J.: Metatheory and Reflection in Theorem Proving: A Survey and Critique, Technical Report CRC-053, SRI Cambridge (1995)
Jones, R.B., O’Leary, J.W., Seger, C.-J.H., Aagaard, M.D., Melham, T.F.: Practical formal verification in microprocessor design. IEEE Design & Test of Computers 18(4), 16–25 (2001)
Kaivola, R., Kohatsu, K.R.: Proof engineering in the large: Formal verification of the Pentium-4 floating-point divider. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 196–211. Springer, Heidelberg (2001)
Kaivola, R., Narasimhan, N.: Formal verification of the Pentium-4 multiplier. In: High-Level Design Validation and Test: 6th International Workshop, HLDVT 2001, pp. 115–122. IEEE Computer Society Press, Los Alamitos (2001)
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer, Dordrecht (2000)
Matthews, J., Cook, B., Launchbury, J.: Microprocessor specification in Hawk. In: IEEE International Conference on Computer Languages, pp. 90–101. IEEE Computer Society Press, Los Alamitos (1998)
O’Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally Verifying IEEE Compliance of Floating-Point Hardware. Intel Technical Journal (First quarter, 1999), Available at developer.intel.com/technology/itj/
Seger, C.-J.H., Bryant, R.E.: Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods in System Design 6(2), 147–189 (1995)
Seger, C.-J.H., Jones, R.B., O’Leary, J.W., Aagaard, M.D., Barrett, C., Syme, D.: An Industrially Effective Environment for Formal Hardware Verification (submitted for publication)
Sheard, T.: Accomplishments and Research Challenges in Meta-Programming. In: Taha, W. (ed.) SAIG 2001. LNCS, vol. 2196, pp. 2–44. Springer, Heidelberg (2001)
Sheard, T., Peyton Jones, S.: Template Meta-Programming for Haskell. In: Chakravarty, M.T.M. (ed.) ACM SIGPLAN Haskell Workshop, pp. 1–16. ACM Press, New York (2002)
Spirakis, G.: Leading-edge and future design challenges: Is the classical EDA ready? In: Design Automation: 40th ACM/IEEE Conference, DAC 2003, p. 416. ACM Press, New York (2003)
Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. SIGPLAN Notices 32(12), 203–217 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Melham, T. (2004). Integrating Model Checking and Theorem Proving in a Reflective Functional Language. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-24756-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21377-2
Online ISBN: 978-3-540-24756-2
eBook Packages: Springer Book Archive