Preface

This volume contains the proceedings of the Eleventh Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '13, a two-day workshop held in Laramie, Wyoming, USA on May 30-31, 2013.

The ACL2 Workshop is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2 and the other theorem provers in the Boyer-Moore family.

The workshop received 15 submissions, consisting of 14 regular papers and one extended abstract. Each submission was reviewed by three Program Committee members and external reviewers. Based on these reviews, 11 papers were accepted for presentation at the workshop.

This year's workshop features an exciting collection of papers on a wide variety of topics, such as new modeling features and reasoning improvements, new user interfaces, better automation for reusing proofs, new approaches to partial functions, and applications of ACL2 to verify hardware (including new areas such as asynchronous and quantum circuits) and GPU algorithms.

The workshop would not be possible without the hard work of many people. We thank the authors and speakers for their excellent submissions. We thank the members of the Program Committee and the external reviewers for their work in assessing and improving the workshop submissions. We thank EasyChair for the use of its excellent conference management software. We thank EPTCS and the arXiv for publishing the workshop proceedings in an open-access format.

May 2013
Ruben Gamboa and Jared Davis

Program Chairs

• Ruben Gamboa, University of Wyoming, USA
• Jared Davis, Centaur, USA

Program Committee

• Carl Eastlund, Northeastern University, USA
• David Greve, Rockwell Collins, USA
• Warren Hunt, University of Texas, USA
• Matt Kaufmann, University of Texas, USA
• Hanbing Liu, AMD, USA
• Panagiotis Manolios, Northeastern University, USA
• Magnus Myreen, University of Cambridge, UK
• David Rager, Battelle Memorial Institute, USA
• Sandip Ray, Intel, USA
• Jose Luis Ruiz Reina, University of Seville, Spain
• David Russinoff, Intel, USA
• Jun Sawada, IBM, USA
• Julien Schmaltz, Open University of the Netherlands, The Netherlands
• Konrad Slind, Rockwell Collins, USA
• Sol Swords, Centaur, USA
• Laurent Thery, INRIA, France

External Reviewers

• Bernard van Gastel
• Sebastiaan Joosten
• Disha Puri

Embedding ACL2 Models in End-User Applications

We present the ACL2 Bridge, a way to reuse ACL2 code in tools written in any mainstream programming language. We have used the ACL2 Bridge to develop a modern web application on top of a 100,000 line ACL2 code base. The ACL2 Bridge could be useful for anyone who wants to develop graphical interfaces for ACL2 itself or for models written in ACL2.

Extended Abstract

With ACL2's strong support for efficient execution, it is natural to imagine taking models and specifications from a formal verification effort and incorporating them into other, ancillary programs. The classic example of this is the idea of reusing a formal processor model as a traditional simulator. More recently, we took the ACL2-based Verilog parsing and translation tool that we wrote to model our hardware modules at Centaur, and reused it in standalone command-line programs like a linter and an equivalence checker. These “side tools” are useful: the linter has found many bugs that testing missed, and the equivalence checker is now popular with our circuit designers. Developing these tools seems like a good way to increase collaboration and get more value out of the theorem proving effort.

We want to make it very easy to reuse ACL2 code in end-user applications. When we just want to write a command-line utility that processes some files, it makes sense to use ACL2 itself as the programming language. But ACL2 is a poor platform for developing almost any other kind of program. It has very little support for working with the file system (copying files, listing directories, checking permissions, and so on), limited multi-threading, no networking and no graphics; it has no libraries for generating parsers, connecting to databases, reading widely-used data formats (JSON, XML, YAML, etc.). We can make up for some of this with raw Lisp, e.g., CCL has nice threading and networking support. But frankly, Lisp is a niche language. It lacks the depth of modern, actively developed, well-documented libraries and frameworks enjoyed by mainstream languages. When development time and cost are at a premium, this may limit the kinds of tools we can develop. Using Lisp can also be deterrent to working with developers from other groups since they usually don't know the language.

What we really want, then, is a good way to embed ACL2 code into programs written in other languages---say Ruby, Java, or Python---that are widely known and have plentiful libraries for files, graphics, networks, threads, databases, and so forth. Ideally, we should be able to choose whatever language best fits the kind of application we want to develop, and then incorporate our ACL2 functions into this language. But here we have a practical problem: how can we effectively integrate ACL2 code into programs written in these other languages?

To solve this problem, we have developed the ACL2 Bridge

The Bridge is implemented as an ACL2 book (see centaur/bridge) with a trust tag. This book extends your ACL2 session with a server that can accept connections from client programs. A typical client program would be, e.g., the graphical interface for an end-user application. Clients can be written in any programming language that supports sockets. They may be local or remote, and multiple clients can simultaneously interact with the same ACL2 session. (Note that the ACL2 Bridge currently requires CCL as the host Lisp.)

Each client interacts with the server through a kind of read-eval-print loop that is designed for programs. Commands and replies are encoded with a simple, easily parsed message format. The client is given full reign over the ACL2 session and can even submit raw Lisp commands. Output from the server is clearly marked so that the client can distinguish between ordinary return values, error messages, and printed output. The client can also tell when the server is ready for another command.

We have implemented an ACL2Bridge class for clients in Ruby (see centaur/bridge/ruby). It encapsulates the low-level details of communicating with the server and interpreting the read-eval-print loop messages. This allows the rest of the Ruby client program to simply invoke ACL2 commands and get the results in an atomic style. Any Lisp errors are converted into proper Ruby exceptions, and printed output from ACL2 commands (e.g., from cw) can be streamed as it is produced or collected for analysis. This class is only 250 lines of code, 140 of which are blank or comments. Even if you want to use some other programming language, it can serve as a useful example of how to write your client.

Our ACL2Bridge class handles the mechanics of communicating with ACL2, but this is only part of the problem. To write an interesting client, we also need to be able to construct Lisp commands and interpret the results. It is generally easy for a client to construct S-expressions to give as commands. But ACL2 objects are normally printed as S-expressions, and most programming languages do not have built-in support for parsing S-expressions. To make it easy to write a client without having to first implement an S-expression parser, the ACL2 bridge can (optionally) encode return values in JSON format. JSON libraries are readily available for every major programming language, and it is an especially convenient format for web applications.

We have used the ACL2 Bridge to develop VL-Mangle, a web-based Verilog refactoring tool. The backend of this tool is written in ACL2, and reuses VL, our large (100,000+ line) ACL2 code-base for working with Verilog. The frontend of the tool is a Web application written in Ruby with the Sinatra microframework. Hardware designers who use the tool are presented with a nice graphical interface within their web browser that lets them mechanically transform whole sets of modules, see what changed, undo and redo transforms, save their progress, etc.

The ACL2 Bridge is a straightforward mechanism for embedding ACL2 code into software written in mainstream languages. This allows us to reuse the modeling and specification work needed to support our formal verification effort to write useful end-user applications. It is easy to imagine using it to develop new graphical interfaces for interacting with the theorem prover, itself. As a simple, multi-threaded connection to ACL2, the ACL2 Bridge might also be useful to the authors of existing interfaces to ACL2, such as the ACL2 Sedan, DrACuLa, and ProofPad.

* This abstract describes work published in DoForm 2013.

Copyright © Jared Davis
This work is licensed under the Creative Commons Attribution License.