ACL2 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. We report on improvements to ACL2 made since the 2013 ACL2 Workshop.

ABSTRACT. The modeling tools, specifications, and proof scripts for an industrial formal verification effort can easily reach hundreds of thousands of lines of source code. High quality documentation is vital for teams that are working on projects of this scale. We have developed a flexible, scalable docu- mentation tool for ACL2 that can incorporate the documentation for the ACL2 theorem prover, the Community Books, and an organization’s internal formal verification projects. The resulting manuals are automatically accurate and current, and are easily deployed throughout an organization.

ABSTRACT. We present a data definition framework that supports a wide variety of specifying (classifying) ``new'' data types from existing types. A distinguishing feature of our approach is that we maintain both a analytic (recognizer/predicate function) and synthetic (enumerator function) characterization of a data definition. We describe the syntax and semantics of our interfacing macros (\p{defdata} et al). The \p{defdata} language concisely captures common data definition patterns, e.g. list types, map types, record types, and installs theories raising the level of automation for reasoning about such types (and associated functions). It also provides support for polymorphic functions, by using the advanced ACL2 features of \p{encapsulate} and functional instantiation, without exposing them to the user. We give a complete characterization (in terms of tau-rules) of the inclusion/exclusion relations a \p{defdata} type definition induces. We present a number of examples illustrating usage of \p{defdata}. The data definition framework has been implemented as a component of counterexample generation support in ACL2 Sedan, but can be independently used, and is available, as a community book.

ABSTRACT. This paper describes a tool suite for the ACL2 programming language which incorporates certain ideas from the Hindley-Milner paradigm of functional programming (as manifested in popular languages like ML and Haskell), including a "typed" style of programming with the ability to define polymorphic types. These ideas are introduced via macros into the language of ACL2, taking advantage of ACL2's guard-checking mechanism to perform type checking on both function definitions and theorems. Finally, we discuss how these macros can be used to implement features of a high-level software specification and implementation language. (citation Specware/Kestrel)

ABSTRACT. ACL2(ml) is an extension for the Emacs interface of ACL2. It uses machine-learning to help the ACL2 user during the proof-development. ACL2(ml) gives hints to the user in the form of families of similar theorems, and generates auxiliary lemmas automatically. In this paper, we present the two most recent extensions for ACL2(ml). First, ACL2(ml) can suggest families of similar definitions, in addition to the families of similar theorems. Second, the lemma generation tool has been improved with a method to generate preconditions based on the guard mechanism of ACL2. The user of ACL2(ml) can also invoke directly the latter extension to obtain preconditions for his conjectures.

ABSTRACT. We present first experiments with translating ACL2 problems to TPTP and running TPTP-style ATPs on such problems.

ABSTRACT. The ForMaRE project (\textbf{for}mal \textbf{ma}thematical \textbf{r}easoning in \textbf{e}conomics) is an interdisciplinary effort with the goal of increasing confidence in theoretical results in economics. In a nutshell, the idea is to find suitable automated reasoning platforms for reasoning about economic theory. This requires collaboration among economists and formal methodists, but in an ideal world, the automated reasoning platforms will become sufficiently advanced that economists can use them directly. As such, researchers in the ForMaRE project recently analyzed the suitability of four different automated reasoning platforms for this project: Isabelle, Theorema, Mizar, and Hets/CASL/TPTP. A major portion of the analysis was the formalization in each of these systems of Vickrey's theorem on the equilibrium and efficiency of second-price auctions. Conspicuously absent from the list of theorem provers considered is ACL2. This paper describes our attempt to rectify this oversight.

ABSTRACT. ACL2(r) is a variant of ACL2 that supports the irrational real and complex numbers. Its logical foundation is based on internal set theory (IST), an axiomatic formalization of non-standard analysis (NSA). Familiar ideas from analysis, such as continuity, differentiability, and integrability, are defined quite differently in NSA---some would argue the NSA definitions are more intuitive. In previous work, we have adopted the NSA definitions in ACL2(r), and simply taken as granted that these are equivalent to the traditional analysis notions, e.g., to the familiar $\epsilon$-$\delta$ definitions. However, we argue in this paper that there are circumstances when the more traditional definitions are advantageous in the setting of ACL2(r), precisely because the traditional notions are classical, so they are unencumbered by IST limitations on inference rules such as induction or the use of pseudo-lambda terms in functional instantiation. To address this concern, we describe a formal proof in ACL2(r) of the equivalence of the traditional and non-standards definitions of these notions.

ABSTRACT. The verification of many algorithms for calculating transcendental functions is based on polynomial approximations to these functions, often Taylor series approximations. However, computing and verifying approximations to the arctangent function are very challenging problems, in large part because the Taylor series converges very slowly to arctangent---a 57th-degree polynomial is needed to get three decimal places for arctan(0.95). Medina proposed a series of polynomials that approximate arctangent with far faster convergence---a 7th-degree polynomial is all that is needed to get three decimal places for arctan(0.95). We present in this paper a proof in ACL2(r) of the correctness and convergence rate of this sequence of polynomials. The proof is particularly beautiful, in that it uses many results from real analysis. Some of these necessary results were proven in prior work, but some were proven as part of this effort.

ABSTRACT. Behavioral synthesis involves compiling an Electronic System-Level (ESL) design into its Register-Transfer Level (RTL) implementation. Loop pipelining is one of the most critical and complex transformations employed in behavioral synthesis. Certifying the loop pipelining algorithm is challenging because there is a huge semantic gap between the input sequential design and the output pipelined implementation making it infeasible to verify their equivalence with automated sequential equivalence checking techniques. We discuss our ongoing effort using ACL2 to certify loop pipelining transformation. The completion of the proof is work in progress. However, some of the insights developed so far may already be of value to the ACL2 community. In particular, we discuss the key invariant we formalized, which is very different from that used in most pipeline proofs. We discuss the needs for this invariant, its formalization in ACL2, and our envisioned proof using the invariant. We also discuss some trade-offs, challenges, and insights developed in course of the project.

ABSTRACT. Proving the correctness of programs written for multiple processors is a challenging proglem, due in no small part to the weaker memory guarantees afforded by most modern architectures. In particular, the existence of store buffers means that the programmer can no longer assume that writes to different locations become visible to all processors in the same order. However, all practical architectures do provide a collection of weaker guarantees about memory consistency across processors, which enable the programmer to write provably correct

ABSTRACT. We describe the formal language MASC, based on a subset of SystemC and intended for modeling algorithms to be implemented in hardware. By means of a special-purpose parser, an algorithm coded SystemC is converted to a MASC model for the purpose of documentation, which in turn is translated to ACL2 for formal verification. The parser also generates a SystemC variant that is suitable as input to a high-level synthesis tool. As an illustration of this methodology, we describe a proof of correctness of a simple 32-bit radix-4 multiplier.

ABSTRACT. In our current work a library of formally verified software components is to be created, and assembled, using the Low-Level Virtual Machine (LLVM) intermediate form, into subsystems whose top-level assurance relies on the assurance of the individual components. We have thus undertaken a project to build a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem prover. Our translator produces executable ACL2 formal models, allowing us to both prove theorems about the translated models as well as validate those models by testing. The resulting models can be translated and certified without user intervention, even for code with loops, thanks to the use of the def::ung macro which allows us to defer the question of termination. Initial measurements of concrete execution for translated LLVM functions indicate that performance is nearly 2.4 million LLVM instructions per second on a typical laptop computer. In this paper we overview the translation process and illustrate the translator's capabilities by way of a concrete example, including both a functional correctness theorem as well as a validation test for that example.