Welcome to my blog. My name is Mark Reitblatt, and I'm an undergraduate in the University of Texas (Austin) Department of Computer Sciences. The purpose of this blog is to document what I learn as I journey into the broad and deep world of Automated Theorem Proving (ATP for short). Hopefully, this will be a useful resource to other students interested in the domain of formal methods, but unsure about where to start.
For the time being, my primary focus will be on the ACL2 theorem prover written by J Moore and Matt Kaufmann. Written in its own logic (based upon Common Lisp), ACL2 is the latest incarnation of the Boyer-Moore theorem prover. In 2006, the Boyer-Moore theorem prover won an ACM Software System Award.
ACL2 has seen extensive use throughout industry, being used to prove the correctness of the floating point division algorithm in the AMD K5 processor, the correctness of the first silicon implementation of the JVM and the correctness of the pipeline hazard detection algorithm of the Motorola CAP DSP, among many other projects. One current project is constructing a model of the Java Virtual Machine in order to prove theorems about programs written in JVM Bytecode.
In my next post I'll talk about my current goals with ACL2, namely my ideas for my Bachelors Honors Thesis.
ACL2 has seen extensive use throughout industry, being used to prove the correctness of the floating point division algorithm in the AMD K5 processor, the correctness of the first silicon implementation of the JVM and the correctness of the pipeline hazard detection algorithm of the Motorola CAP DSP, among many other projects. One current project is constructing a model of the Java Virtual Machine in order to prove theorems about programs written in JVM Bytecode.
In my next post I'll talk about my current goals with ACL2, namely my ideas for my Bachelors Honors Thesis.
No comments:
Post a Comment