Abstract
In my view, the “verification problem” is the theorem proving problem, restricted to a computational logic. My approach is: adopt a functional programming language, build a general purpose formal reasoning engine around it, integrate it into a program and proof development environment, and apply it to model and verify a wide variety of computing artifacts, usually modeled operationally within the functional programming language. Everything done in this approach is software verification since the models are runnable programs in a subset of an ANSI standard programming language (Common Lisp). But this approach is of interest to proponents of other approaches (e.g., verification of procedural programs or synthesis) because of the nature of the mathematics of computing. I summarize the progress so far using this approach, sketch the key research challenges ahead and describe my vision of the role and shape of a useful verification system.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Bevier, W.R.: A verified operating system kernel. Ph.d. dissertation, University of Texas at Austin (1987)
Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: Special issue on system verification. Journal of Automated Reasoning 5(4), 409–530 (1989)
Boyer, R.S., Moore, J.S.: Proving theorems about pure lisp functions. J. ACM 22(1), 129–144 (1975)
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)
Boyer, R.S., Moore, J.S.: A mechanical proof of the unsolvability of the halting problem. Journal of the Association for Computing Machinery 31(3), 441–458 (1984)
Boyer, R.S., Moore, J.S.: Proof checking the rsa public key encryption algorithm. American Mathematical Monthly 91(3), 181–189 (1984)
Boyer, R.S., Moore, J.S.: Mjrty – a fast majority vote algorithm. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 105–117. Kluwer Academic Publishers, Automated Reasoning Series, Dordrecht (1991)
Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, Second Edition. Academic Press, New York (1997)
Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, Springer, Heidelberg (2002), http://www.cs.utexas.edu/users/moore/publications/stobj/main.ps.gz
Boyer, R.S., Moore, J.S., Green, M.W.: The use of a formal simulator to verify a simple real time control program. In: Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra, pp. 54–66. Springer, Heidelberg (1990) (Texts and Monographs in Computer Science)
Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. Journal of the ACM 43(1), 166–192 (1996)
Brock, B., Hunt Jr., W.A.: Formal analysis of the motorola CAP DSP. In: Industrial-Strength Formal Methods, Springer, Heidelberg (1999)
Brock, B., Moore, J.S.: A mechanically checked proof of a comparator sort algorithm. In: Engineering Theories of Software Intensive Systems, IOS Press, Amsterdam (to appear, 2005)
Flatau, A.D.: A verified implementation of an applicative language with dynamic storage allocation. Ph.d. thesis, University of Texas at Austin (1992)
Goldberg, J., Kautz, W., Mellear-Smith, P.M., Green, M., Levitt, K., Schwartz, R., Weinstock, C.: Development and analysis of the software implemented fault-tolerance (sift) computer. Technical Report NASA Contractor Report 172146, NASA Langley Research Center, Hampton, VA (1984)
Greve, D., Wilding, M.: Evaluatable, high-assurance microprocessors. In: NSA High-Confidence Systems and Software Conference (HCSS), Linthicum, MD (March 2002), http://hokiepokie.org/docs/hcss02/proceedings.pdf
Greve, D., Wilding, M.: A separation kernel formal security policy (2003)
Greve, D.A.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 203–203. Springer, Heidelberg (1998)
Hunt, W.A.: FM8501: A Verified Microprocessor. LNCS, vol. 795. Springer, Heidelberg (1994)
Hunt, W.A., Brock, B.: A formal HDL and its use in the FM9001 verification. In: Proceedings of the Royal Society (April 1992)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)
Kaufmann, M., Moore, J.S.: Some key research problems in automated theorem proving for hardware and software verification. Revista de la Real Academia de Ciencias (RACSAM) 98(1), 181–196 (2004)
Kaufmann, M., Moore, J.S.: The ACL2 home page. In: Dept. of Computer Sciences, University of Texas at Austin (2006), http://www.cs.utexas.edu/users/moore/acl2/
Kernighan, B.W., Ritchie, D.M.: The C Programming Language, Second Edition. Prentice Hall, Englewood Cliff (1988)
Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: A study. In: Workshop on Interpreters, Virtual Machines and Emulators 2003 (IVME 2003), San Diego, CA, ACM SIGPLAN, New York (2003)
McCune, W., Shumsky, O.: Ivy: A preprocessor and proof checker for first-order logic. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, Boston, MA, pp. 265–282. Kluwer Academic Press, Dordrecht (2000)
Moore, J.S.: Piton: A Mechanically Verified Assembly-Level Language. In: Automated Reasoning Series, Kluwer Academic Publishers, Dordrecht (1996)
Moore, J.S.: Proving theorems about Java and the JVM with ACL2. In: Broy, M., Pizka, M. (eds.) Models, Algebras and Logic of Engineering Software, pp. 227–290. IOS Press, Amsterdam (2003), http://www.cs.utexas.edu/users/moore/publications/marktoberdorf-03
Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Transactions on Computers 47(9), 913–926 (1998)
Moore, J.S., Porter, G.: The Apprentice challenge. ACM TOPLAS 24(3), 1–24 (2002)
Ray, S., Moore, J.S.: Proof styles in operational semantics. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 67–81. Springer, Heidelberg (2004)
Russinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. London Mathematical Society Journal of Computation and Mathematics 1, 148–200 (1998), http://www.onr.com/user/russ/david/k7-div-sqrt.html
Sawada, J.: Formal verification of divide and square root algorithms using series calculation. In: Proceedings of the ACL2 Workshop, 2002 (April 2002), http://www.cs.utexas.edu/users/moore/acl2/workshop-2002
Shankar, N.: Metamathematics, Machines, and Godel’s Proof. Cambridge University Press, Cambridge (1994)
Smith, S.W., Austel, V.: Trusting trusted hardware: Towards a formal model for programmable secure coprocessors. In: The Third USENIX Workshop on Electronic Commerce (September 1998)
Sumners, R.: Correctness proof of a BDD manager in the context of satisfiability checking. In: Proceedings of ACL2 Workshop 2000. Department of Computer Sciences, Technical Report TR-00-29 (November 2000), http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/final/sumners2/paper.ps
Wilding, M.: Nim game proof. Technical Report CLI Tech Report 249, Computational Logic, Inc. (November 1991), http://www.cs.utexas.edu/users/boyer/ftp/nqthm/nqthm-1992/examples/numbers/nim.eventsq
Young, W.D.: A verified code generator for a subset of Gypsy. Technical Report 33, Comp. Logic. Inc. Austin, Texas (1988)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Moore, J.S. (2008). A Mechanized Program Verifier. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)