Wednesday, November 14

6:00-9:00

Banquet

Thursday, November 15

Welcome

8:50-9:00

Welcome

Session 1, Chair: John Cowles

9:00-9:30

Hacking and Extending ACL2

Peter Dillinger, Matt Kaufmann, Pete Manolios

Slides

9:30-10:00

Pythia: Automatic Generation of Counterexamples for ACL2 using Alloy

Alexander Spiridonov, Sarfraz Khurshid

Slides

10:00-10:20

Backtracking and Induction in ACL2

John Erickson

Slides

Session 2, Chair: John Matthews

10:40-11:00

The While-language Challenge: First Progress

John Cowles, David Greve, William Young

Prelude | Slides

11:00-11:20

Building Lemmas Using Examples

Gabriel Infante-Lopez

Slides

Invited Talk, Chair: Jun Sawada

1:00-2:00

Mechanized Metamathematics Revisited

Natarajan Shankar

Slides

Session 3, Chair: Warren Hunt

2:20-2:40

Formalizing Simplicial Topology in ACL2

Mirian Andres, Laureano Lamban, Julio Rubio, Jose Luis Ruiz-Reina

Slides

2:40-3:10

Formal Specification and Validation of Minimal Routing Algorithms for the 2D Mesh

Julien Schmaltz

Slides

Session 4, Chair: Ruben Gamboa

3:30-4:00

Circuit Specification, Abstraction, and Reverse Engineering

Warren Hunt, Robert S. Boyer

Slides

4:00-4:20

Defining a LISP Interpreter in a Logic of Total Functions

Mike Gordon

Slides

Rump Session 1, Chair: Rex Page

4:40-5:00

Foundations of Automated Induction for a Structured Mechanized Logic

Matt Kaufmann, J Moore, Sandip Ray

Slides

5:00-5:20

Termination Analysis with Calling Context Graphs

Pete Manolios, Daron Vroon

Slides

5:20-5:35

Combining Deductive Reasoning and Decision Procedures for System-Level Verification

Sudarshan Srinivasan, Pete Manolios

Slides

5:35-5:50

Verifying NoC communication architectures with ACL2

Julien Schmaltz, Laurence Pierre, Amr Helmy

Slides

5:50-6:05

Automating Formal Verification of Block Ciphers

Eric Smith

Slides

Friday, November 16

Welcome

8:50-9:00

Welcome

Session 5, Chair: Matt Kaufmann

9:00-9:30

ACL2 for Freshmen: First Experiences

Carl Eastlund, Dale Vaillancourt, Matthias Felleisen

Slides

9:30-10:00

Evolution from Debugging to Verification

Frank Rimlinger

10:00-10:30

Scalable Normalization for Heap Manipulating Functions

David Greve

Slides

Update

10:50-11:20

What's New in ACL2?

Matt Kaufmann

Notes

Invited Talk, Chair: J Strother Moore

1:00-2:00

A Vision for Verification in LabVIEW

Jeff Kodosky

Slides

Rump Session 2, Chair: Pete Manolios

2:20-2:30

A Generalized Solution for the While Challenge

Sandip Ray

Slides

2:30-2:40

Pushing the While Language Challenge to Greater Depths

John Cowles

Slides

2:40-2:50

Red-Black Trees for DrACuLa

Ruben Gamboa

Slides | Materials

2:50-3:05

Formal Verification of LabVIEW Programs with ACL2

Matt Kaufmann, Jacob Kornerup, Grant Passmore

Slides | Example

3:05-3:20

Proof reusing: the case of the Hindley algorithm

Diego Sotes, Laureano Lamban, Julio Rubio

Slides

Rump Session 3, Chair: Dave Greve

3:40-3:50

Specifying the X86 ISA

Warren Hunt

Slides

3:50-4:05

The Milawa rewriter and an ACL2 proof of its soundness

Jared Davis

Slides

4:05-4:15

Using ACL2's Verified Clause Processor Mechanism to Sort Commutative and Associative Operations

Erik Reeber

Slides

4:15-4:30

ACL2s, the ACL2 Sedan

Peter Dillinger, Pete Manolios, Daron Vroon, J Moore

Slides

Discussion

4:35-5:25

Work Session

Matt Kaufmann