ACL2 Workshop 2015 Rump Session Abstracts

We present our system (currently in development) for correct-by-construction software generation using ACL2. Our system includes a growing library of proof-producing transformations (e.g., to change a function to be tail recursive, or to apply a finite-differencing optimization). The transformations are implemented using ACL2's make-event and can transform a high-level specification into lower-level, more efficient code -- with proofs emitted along the way. We have also developed other techniques for software synthesis by verified refinement. For example, a high-level declarative specification can be refined by applying an algorithm scheme such as divide-and-conquer. Our system also includes an implementation, in ACL2, of specifications and specification morphisms in the style of Kestrel's Specware system. Implemented using ACL2's notions of encapsulate and functional instantiation, these provide convenient constructs for refinement-based software synthesis.

We conjecture that some of the techniques we are developing may be useful for verification as well as synthesis.

This summer I largely took a break from ACL2 and returned to my roots as a mathematical logician. To my surprise, a lemma arose in a model theory paper I'm co-authoring that could be abstracted to something amenable to a straightforward formalization in ACL2. To my dismay, it took me approximately 2 full days (16 hours, actually spread over many days) to complete that exercise.

In this talk I will describe the result, sketch its informal proof, and challenge the community to do a better and faster job on the ACL2 proof than I did! Possible approaches may include structured development methodologies and better tools for searching libraries. I may also discuss a few things that I may have done right. Finally, I'll point to a file of definitions and the desired theorem (books/demos/proofs/tightness-lemma.lisp and books/demos/proofs/tightness-lemma-proof.lisp), and put forward the challenge to do a better job than I did in proving that theorem. Perhaps we could have a future workshop session that compares solutions?

Curve255219 is an elliptic curve Diffie-Hellman function that has achieved new speed records and is used in a variety of high-security encryption applications. As a very first step in the formalization and proof of correctness of a proposed hardware implementation of this function, I'll describe an ACL2 proof of the primality of 2^255-19 based on Pratt certification.

We present our work using the ACL2 theorem prover to formally model the Android platform and to formally verify Android apps. Our approach allows the verification of the full functional correctness of apps (e.g., that a calculator app computes the correct numeric result) as well as security properties (e.g., that an app only sends data to certain URLs). Verifying an app with our system provides high assurance that it satisfies its specification.

Android is an event-driven system. Our formal model is an executable simulator of a growing subset of the Android platform, and app proofs are done by automated symbolic execution of the app's event handlers using the formal model. By induction, we prove that an app satisfies an invariant, including the correctness properties of interest, for all possible sequences of events. To our knowledge, our formal Android model is the most detailed and our Android app verification is the most thorough, compared to other approaches.

I have an implementation of a LOOP-like macro for executing iterative statements at the top-level of the ACL2 loop. It handles the Common Lisp iteration primitives FOR, AS, IN, ON, FROM, DOWNFROM, UPFROM, TO, DOWNTO, UPTO, BELOW, ABOVE, BY, WHEN, UNLESS, WHILE, UNTIL, ALWAYS, NEVER, THEREIS, COLLECT, APPEND, COUNT, MAXIMIZE, MINIMIZE, and SUM. It is compatible with the Common Lisp standard on these primitives, but Common Lisp provides additional primitives that my package does not currently support. Most of the excluded Common Lisp primitives involve unsupportable features (like destructive modification or side-effects). Furthermore, the recursive functions introduced by my macro are in :PROGRAM mode and are local -- they disappear as soon as the loop has been executed. I'll demonstrate the macro and we can discuss the issues involved in extending translate to support :LOGIC mode, proofs, and decent prettyprinting.

def::ung is a "defun wrapper" that allows the user to admit arbitrary recursive function definitions without justifying termination. I will discuss the recent addition of multiple-value and stobj support as well as efforts to streamline the underlying theory and enhance robustness.

We have had an open source contribution system in place for many years now. Embracing modern version control technology, we've recently moved to hosting our source code on github. We welcome and encourage contributions to this repository! This rump talk will introduce the github repository to the community. This rump talk will also introduce our build server, http://leeroy.defthm.com, to the community, and we will discuss the benefits of the build server and the workflow that we have setup to accept contributions to our community source code.