ACL on Wednesday, August 16th

Session 5 (09:00‑10:30)
Chair: Matt Kaufmann

09:00‑09:30	Erik Reeber (University of Texas at Austin) Jun Sawada (IBM Austin Research Laboratory) Combining ACL2 and an Automated Verification Tool to Verify a Multiplier We have extended the ACL2 theorem prover to automatically prove properties of VHDL circuits with IBM's Internal SixthSense verification system. We have used this extension to verify a multiplier used in an industrial floating point unit. The property we ultimately verify corresponds to the correctness of the component that produces a pair of bit-vectors whose summation is equal to the product. This property is beyond the scale of the SixthSense system alone. In this paper we show how we verified the multiplier by illustrating key ACL2 lemmas and theorems, and also properties checked by SixthSense.
09:30‑10:00	Ruben Gamboa (University of Wyoming) John Cowles (University of Wyoming) Implementing a Cost-Aware Evaluator for ACL2 Expressions One of ACL2's most interesting features is that it is executable, so users can run the programs that they verify, and debug them during verification. In fact, the ACL2 implementors have gone well out of their way to make sure ACL2 programs can be executed efficiently. Nevertheless, ACL2 does not provide a framework for reasoning about the cost of function invocations. This paper describes how such a framework can be added to ACL2, by using ACL2 macros and supporting Common Lisp code to access the prover state.
10:00‑10:30	Robert S. Boyer (University of Texas) Warren A. Hunt, Jr. (University of Texas at Austin) Function Memoization and Unique Object Representation for ACL2 Functions We have developed an extension of ACL2 that includes the implementation of hash-based association lists and function memoization; this makes some algorithms execute more quickly. This extension, enabled partially by the implementation of Hash-CONS, represents ACL2 objects in a canonical way, thus the comparison of any two such objects can be determined without the cost of descending through their CONS structures. A restricted set of ACL2 user-defined functions may be memoized; the underlying implementation may conditionally retain the values of such function calls so that if a repeated function application is requested, a previously computed value may instead be returned. We have defined a fast association list access and update functions using hash tables. We provide a file reader that identifies and eliminates duplicate representations of repeated objects, and a file printer that produces output with no duplicate subexpressions.

Break (10:30‑11:00)

Session 6 (11:00‑12:00)
Chair: Ruben Gamboa

11:00‑11:15	David L. Rager (The University of Texas at Austin Computer Science) Adding Parallelism Capabilities to ACL2 We have implemented parallelism primitives that permit an ACL2 programmer to parallelize execution of ACL2 functions. We (1) introduce logical definitions for these primitives, (2) explain the features of our extension, (3) give an evaluation strategy for our implementation, and (4) use the parallelism primitives in examples to show speedup.
11:15‑11:30	Sandip Ray (University of Texas at Austin) Quantification in Tail-recursive Function Definitions We investigate the logical issues behind axiomatizing equations that contain both recursive calls and quantifiers in ACL2. We identify a class of such equations, named extended tail-recursive equations, that can be uniformly introduced in the logic. We point out some practical benefits of this axiomatization, and discuss the logical impediments behind introducing more general quantified formulas.
11:30‑11:45	Warren A. Hunt, Jr. (University of Texas at Austin) Serita M. Nelesen (The University of Texas at Austin) Phylogenetic Trees in ACL2 Biologists studying the evolutionary relationships between organisms use heuristic searches to attempt to find the correct phylogenetic tree. However, these searches often produce large collections of trees that the biologist saves in Newick format in order to perform further analysis. Unfortunately, Newick is neither space efficient, nor conducive to post-tree analysis such as consensus. We propose a new format for storing phylogenetic trees that significantly reduces storage requirements while continuing to allow the trees to be used as input to post-tree analysis. We implemented mechanisms to read and write such data from and to files, and also implemented a consensus algorithm that is faster by an order of magnitude than standard phylogenetic analysis tools. We demonstrate our results on a collection of data files produced from both maximum parsimony tree searches and Bayesian methods.
11:45‑12:00	Matt Kaufmann (University of Texas) J Strother Moore (University of Texas at Austin) Double Rewriting for Equivalential Reasoning in ACL2 Several users have had problems using equivalence-based rewriting in ACL2 because the ACL2 rewriter caches its results. We describe this problem in some detail, together with a solution first implemented in ACL2 Version 2.9.4. The solution consists of a new primitive, double-rewrite, together with a new warning to suggest possible use of this primitive.

Rump Session (Part of Session 6) (12:00‑13:30)

12:00‑12:05	Bill Bevier and David Russinoff Formally Modeling the x86 Instruction Set Architecture
12:05‑12:10	Warren Hunt BDDs
12:10‑12:15	Peter Dillinger, Pete Manolios, J Strother Moore, and Daron Vroon ACL2s: The ACL2 Sedan
12:15‑12:20	J Strother Moore Semi-Automatic Functional Instantiation
12:20‑12:25	David Russinoff A Unified Mathematical Theory of Register-Transfer Logic and Computer Arithmetic
12:25‑12:30	Matt Kaufmann, Pete Manolios, J Strother Moore, and Daron Vroon Adding Calling Context Graphs to ACL2 for Improved Termination Analysis

Lunch break (12:30‑14:00)

Session 7 (14:00‑15:30)
Chair: David Russinoff

14:00‑14:30	Dale Vaillancourt (Northeastern University) Rex Page (Oklahoma University) Matthias Felleisen (Northeastern University) ACL2 in DrScheme Teaching undergraduates to develop software in a formal framework such as ACL2 poses two immediate challenges. First, students typically do not know applicative programming and are often unfamiliar with ACL2's syntax. Second, for motivational reasons, students prefer to work on projects that involve designing interactive, graphical applications. In this paper, we present DrACuLa, a pedagogic programming environment that partially solves these problems. The environment adds a subset of Applicative Common Lisp to DrScheme, an integrated programming environment for Scheme. DrACuLa thus inherits DrScheme's pedagogic capabilities, especially its treatment of syntax and run-time errors. Further, DrACuLa also comes with a library for programming interactive, graphical games. The library interface forces students to think of a graphical user interface in terms of state-transition functions, enabling them later to prove theorems about their games in ACL2. DrACuLa provides a graphical front-end to the ACL2 theorem prover for this purpose. In short, DrACuLa allows the formulation of student projects that represent an important intermediate point between data structure exercises in theorem proving and industrial applications.
14:30‑15:00	Jared Davis (University of Texas at Austin) Reasoning about ACL2 File Input We introduce the logical story behind file input in ACL2 and discuss the types of theorems that can be proven about file-reading 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.
15:00‑15:30	Erik Reeber (University of Texas at Austin) Warren A. Hunt, Jr. (University of Texas at Austin) A SAT-Based Procedure for Verifying Finite State Machines in ACL2 We describe a new procedure for verifying ACL2 properties about finite state machines (FSMs) using satisfiability (SAT) solving. We present an algorithm for converting ACL2 conjectures into conjunctive normal form (CNF), which we then output and check with an external satisfiability solver. The procedure is directly available as an ACL2 proof request. When the SAT tool is successful, a theorem is added to the ACL2 system database as a lemma for use in future proof attempts. When the SAT tool is unsuccessful, we use its output to construct a counter-example to the original ACL2 property.

Break (15:30‑16:00)

Session 8 (16:00‑17:30)
Chair: Warren Hunt

16:00‑16:45	Matt Kaufmann, J Strother Moore, All Discussion on Possible Future Enhancements to ACL2
16:45‑17:30	Pete Manolios, Matt Wilding, All Business Meeting