next day
all days

View: session overviewtalk overviewside by side with other conferences

09:00-10:15 Session 14: Improvements to ACL2
Location: FH, Hörsaal 7
Industrial-Strength Documentation for ACL2
SPEAKER: Jared Davis

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.

Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
SPEAKER: Matt Kaufmann

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

10:15-10:45Coffee Break
10:45-13:00 Session 16C: Datatypes and machine learning
Location: FH, Hörsaal 7
Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
SPEAKER: unknown

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

Polymorphic Types In ACL2
SPEAKER: unknown

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)

Data Definitions in ACL2 Sedan

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.

ACL2(ml): Machine-Learning for ACL2
SPEAKER: unknown

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.

13:00-14:30Lunch Break
14:30-16:00 Session 18C: Keynote Mike Gordon
Location: FH, Hörsaal 7
Linking ACL2 and HOL: past achievements and future prospects
SPEAKER: Mike Gordon

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.

16:00-16:30Coffee Break
16:30-19:00 Session 20C: Economics, Rump Sessions and Business Meeting
Location: FH, Hörsaal 7
On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
SPEAKER: unknown

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.