Functional formal methods
Abstract
Some functional programming languages are also mathematical logics. One can reason formally, traditionally, and directly about programs in such languages. This is driving a new application area for functional programming: modeling microarchitectures, hardware design languages, and imperative programming languages. Such models serve the dual purposes of simulation and formal analysis.ACL2, "<u>A</u> <u>C</u>omputational <u>L</u>ogic for <u>A</u>pplicative <u>C</u>ommon <u>L</u>isp," is a functional programming language that is also a first-order mathematical logic supported by a Boyer-Moore style mechanical theorem prover [5]. It is being used to model and verify artifacts of commercial and industrial interest..Other examples are reported in [4].Execution efficiency for industrial-scale simulators, in combination with adherence to an axiomatic semantics, has forced some novel implementation features [1]. In addition, the ACL2 theorem prover is coded in ACL2 and so represents a significant application of functional programming.
The register-transfer level circuit descriptions for the elementary floating-point arithmetic on the AMD Athlon microprocessor were modeled in ACL2. These models were tested on millions of floating-point test vectors as part of the Athlon validation. In addition, the models were mechanically proved to satisfy the IEEE floating-point specifications. Bugs were found before fabrication. The Athlon that you buy has verified floating-point circuitry in it [7].
Avionics microprocessors produced by Rockwell Collins have been modeled in ACL2. Those models have been used as pre-fabrication simulation test benches. In addition, theorems relating various microprocessor models have been proved mechanically [3].
An executable pipeline-level model of the Motorola CAP digital signal processor was proved to implement a sequential microcode engine and microcoded DSP programs were verified [2].
An executable model of the Java Virtual Machine has been used to prove functional correctness of some simple Java classes, including a safety property for a multi-threaded class [6].
References
[1]
R. S. Boyer and J. S. Moore. Single-threaded objects in ACL2. In PADL 2002, pages 9--27, Heidelberg, 2002. http://www.cs.utexas.edu/users/moore/publications/stobj/main.ps.Z.
[2]
Bishop Brock and Warren A. Hunt, Jr. Formal analysis of the motorola CAP DSP. In Industrial-Strength Formal Methods. Springer-Verlag, 1999.
[3]
D. Greve and M. Wilding. Evaluatable, high-assurance microprocessors. In NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, MD, March 2002. http://hokiepokie.org/docs/hcss02/proceedings.pdf.
[4]
M. Kaufmann, P. Manolios, and J. S. Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, Boston, MA., 2000.
[5]
M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston, MA., 2000.
[6]
J. S. Moore and G. Porter. The apprentice challenge. ACM TOPLAS, 24(3):1--24, May 2002.
[7]
D. M. Russinoff and A. Flatau. Rtl verification: A floating-point multiplier. In Kaufmann et al. {4}, pages 201--232.
Recommendations
Functional formal methods
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programmingSome functional programming languages are also mathematical logics. One can reason formally, traditionally, and directly about programs in such languages. This is driving a new application area for functional programming: modeling microarchitectures, ...
A Practical Methodology for the Formal Verification of RISC Processors
In this paper a practical methodology for formally verifying RISC cores is presented. Using a hierarchical model which reflects the abstraction levels used by designers of real RISC processors, proofs between neighboring levels are performed for ...
Theorem Prover for Intuitionistic Logic Based on the Inverse Method
The first-order intuitionistic logic is a formal theory from the family of constructive logics. In intuitionistic logic, it is possible to extract a particular example x = a and a proof of a formula P(a) from a proof of a formula źxP(x). Owing to this ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2002294 pages
Copyright © 2002 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 17 September 2002
Published in SIGPLAN Volume 37, Issue 9
Check for updates
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 377Total Downloads
- Downloads (Last 12 months)1
- Downloads (Last 6 weeks)0
Reflects downloads up to 05 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in