View: session overviewtalk overviewside by side with other conferences

10:45 | Modeling Algorithms in SystemC and ACL2 SPEAKER: John O'Leary 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 in 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. |

11:15 | Development of a Translator from LLVM to ACL2 SPEAKER: unknown 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 \texttt{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. |

11:45 | An ACL2 Mechanization of an Axiomatic Framework for Weak Memory SPEAKER: Benjamin Selfridge 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 |

12:15 | Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis SPEAKER: unknown 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. |

14:30 | Machine-code verification: experience of tackling medium-sized case studies using 'decompilation into logic’ SPEAKER: Magnus Myreen ABSTRACT. All software executes in the form of machine code. Ideally, software verification should reach down to precise statements about the concrete machine code that runs. During my PhD, I developed infrastructure in the HOL4 theorem prover for verification of programs at the level of machine code. The infrastructure includes a programming logic and a proof-producing decompiler and compiler. In the subsequent five years, this infrastructure has been used in two medium-sized case studies: construction of a verified implementation of read-eval-print loop for Lisp, which can run Jared Davis' Milawa prover; and verification of the accuracy of the GCC compiler's output for the C implementation of the seL4 microkernel. These case studies resulted in HOL4 theorems about thousands of lines of concrete x86-64 and ARM machine code, respectively. In this talk, I will explain the existing infrastructure for machine-code verification; describe how the infrastructure had to adapt to the case studies; and reflect on future research directions. This talk describes work done in collaboration with Anthony Fox (ARM ISA specification), Jared Davis (Milawa theorem prover), Thomas Sewell and Gerwin Klein (seL4 microkernel). |