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 report on improvements to ACL2 made since the 2013 ACL2 Workshop.

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

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. 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. 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. Over the years there have been several attempts to obtain the amazing automation and efficiency of ACL2 theorem proving within various versions of the HOL proof assistant. These include building a Boyer-Moore waterfall as a tactic, dynamically linking to ACL2 using the PROSPER Plug-In Interface and, most recently, embedding the ACL2 logic in the HOL logic and then using ACL2 as an trusted oracle. These activities have differed in goals and methods, e.g. placing different emphases on useability, efficiency and logical coherence. The talk will start with a critical historical overview, and will end with thoughts on possible future projects.

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.