Publications

2011

Sol Swords and Jared Davis. Bit-Blasting ACL2 Theorems. ACL2 '2011. (To Appear)

Abstract. Interactive theorem proving requires a lot of human guidance. Proving a property involves (1) figuring out why it holds, then (2) coaxing the theorem prover into believing it. Both steps can take a long time. We explain how to use GL, a framework for proving finite ACL2 theorems with BDD- or SAT-based reasoning. This approach makes it unnecessary to deeply understand why a property is true, and automates the process of admitting it as a theorem. We use GL at Centaur Technology to verify execution units for x86 integer, MMX, SSE, and floating-point arithmetic.

(See also ACL2 '11 Slides)

Magnus O. Myreen and Jared Davis. A Verified Runtime for a Verified Theorem Prover. In Interactive Theorem Proving (ITP 2011). August, 2011, Nijmegen, The Netherlands. Springer, LNCS 6898. Pages 265-280.

Abstract. Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the correctness of runtime systems for programming languages like ML, OCaml or Common Lisp. These runtime systems are complex and critical to the integrity of the theorem provers.
In this paper, we present a new Lisp runtime which has been formally veried and can run the Milawa theorem prover. Our runtime consists of 7,500 lines of machine code and is able to complete a 4 gigabyte Milawa proof effort. When our runtime is used to carry out Milawa proofs, less unveried code must be trusted than with any other theorem prover.
Our runtime includes a just-in-time compiler, a copying garbage collector, a parser and a printer, all of which are HOL4-veried down to the concrete x86 code. We make heavy use of our previously developed tools for machine-code verication. This work demonstrates that our approach to machine-code verication scales to non-trivial applications.

(See also Milawa's Website)

(See also ACL2 '11 Rump Session Slides)

Anna Slobadova, Jared Davis, Sol Swords, and Warren A Hunt., Jr. A Flexible Formal Verification Framework for Industrial Scale Validation. Invited talk, Formal Methods and Models for Codesign (MemoCode 2011). July, 2011. Cambridge, UK.

Abstract. In recent years, leading microprocessor companies have made huge investments to improve the reliability of their products. Besides expanding their validation and CAD tools teams, they have incorporated formal verification methods into their design flows. Formal verification (FV) engineers require extensive training, and FV tools from CAD vendors are expensive. At first glance, it may seem that FV teams are not affordable by smaller companies. We have not found this to be true. This paper describes the formal verification framework we have built on top of publicly-available tools. This framework gives us the flexibility to work on myriad different problems that occur in microprocessor design.

2010

Warren A. Hunt Jr., Sol Swords, Jared Davis, and Anna Slobadova. Use of Formal Verification at Centaur Technology. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High Assurance Applications. 2010. Springer. Pages 65-88.

2009

Jared Davis. A Self-Verifying Theorem Prover. Ph.D. Dissertation. The University of Texas at Austin. December, 2009

Abstract. Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier?
We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true").
Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higherlevel proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified.
To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some Phi, there exists a Level 1 proof of Phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof. That is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs.
In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1.

(See also Milawa's Website)

2006

Jared Davis. Memories: Array-like Records for ACL2. In ACL2 2006. August, 2006, Seattle, WA, USA.

Abstract. We have written a new records library for modelling fixed-size arrays and linear memories. Our implementation provides fixnum-optimized O(log₂ n) reads and writes from addresses 0, 1, ... , n-1. Space is not allocated until locations are used, so large address spaces can be represented. We do not use single-threaded objects or ACL2 arrays, which frees the user from syntactic restrictions and slow-array warnings. Finally, we can prove the same hypothesis-free rewrite rules found in misc/records for efficient rewriting during theorem proving.

(See also Memory Library Website)

Jared Davis. Reasoning about File Input in ACL2. In ACL2 2006. August, 2006, Seattle, WA, USA.

Abstract. We introduce the logical story behind file input in ACL2 and discuss the types of theorems that can be proven about filereading operations. We develop a low level library for reasoning about the primitive input routines. We then develop a representation for Unicode text, and implement efficient functions to translate our representation to and from the UTF-8 encoding scheme. We introduce an efficient function to read UTF-8-encoded files, and prove that when files are well formed, the function produces valid Unicode text which corresponds to the contents of the file.
We find exhaustive testing to be a useful technique for proving many theorems in this work. We show how ACL2 can be directed to prove a theorem by exhaustive testing.

(See also Input Library Website)

2004

Jared Davis. Finite Set Theory based on Fully Ordered Lists. In ACL2 2004. November, 2004, Austin, TX, USA.

Abstract. We present a new finite set theory implementation for ACL2 wherein sets are implemented as fully ordered lists. This order unifies the notions of set equality and element equality by creating a unique representation for each set, which in turn enables nested sets to be trivially supported and eliminates the need for congruence rules.
We demonstrate that ordered sets can be reasoned about in the traditional style of membership arguments. Using this technique, we prove the classic properties of set operations in a natural and effotless manner. We then use the exciting new MBE feature of ACL2 to provide linear-time implementations of all basic set operations. These optimizations are made "behind the scenes" and do not adversely impact reasoning ability.
We finally develop a framework for reasoning about quantification over set elements. We also begin to provide common higher-order patterns from functional programming. The net result is an efficient library that is easy to use and reason about.

(See also Sets Library Website)

Gregory L. Wickstrom, Jared Davis, Steve Morrison, Steve Roach, Victor L. Winter. The SSP: An Example of High-Assurance Systems Engineering. In High-Assurance Systems Engineering (HASE 2004). March, 2004, Tampa, FL, USA. IEEE Computer Society 2004, ISBN 0-7695-2094-4.

Abstract. The SSP is a high assurance systems engineering effort spanning both hardware and software. Extensive design review, first principle design, n-version programming, program transformation, verification, and consistency checking are the techniques used to provide assurance in the correctness of the resulting system.