ACL2 Theorem Proving Seminar at the University of Texas

ACL2 stands for ``A Computational Logic for Applicative Common Lisp'' but our research group is interested in all aspects of mechanized theorem proving and in the mechanized verification of hardware and software.

This page lists meetings back to the start of the 2002-2003 academic year.

Click here for some formal methods papers (for possible future presentations).

---

Upcoming meetings:

• None currently scheduled.

Miscellaneous related talks:

• 11-9-20
  Carl Kwan: "A Brief Introduction to Smtlink".
  [Slides]

Previous meetings (reverse order):

• 4/30/19
  Special meeting: PhD dissertation defense of Cuong Chau, 3:00 pm (in the usual room, GDC 7.808)
  [Title and Abstract]
• 4/19/19
  Matt Kaufmann will give two short talks:
  [Abstracts]
  • Iteration in ACL2
    [Slides (no pauses)] [Slides (with pauses)]
  • What's New in ACL2 Version 8.2
    [Version 8.2 Release notes]
• 4/5/19
  Matt Kaufmann will talk: "ACL2: Implementation of a Computational Logic".
  [Abstract, Slides, and Demos]
• 3/29/19
  Mertcan Temel will talk: "RP-Rewriter: A Knowledge Preserving Rewriter to Reduce Backchaining".
  [Abstract] [Slides] [Demo]
• 3/15/19
  Cuong Chau will talk: "A Hierarchical Approach to Asynchronous Circuit Modeling and Verification Using the DE System".
  [Abstract] [Slides]
• 3/8/19
  Marijn Heule will talk: "Solving Hard Problems Automatically".
  [Abstract]
• 3/1/19
  General Roundtable
• 2/1/19
  Curtis Dunham will speak: "An Introduction to Agda".
  [Abstract] [Slides (PDF)] [Slides (PowerPoint)]
• 1/25/19
  J Moore will speak on incorporating the Common Lisp LOOP macro into ACL2.
  [Abstract] [Session Log]
• 12/07/18
  Mertcan Temel will talk: Formal Verification of Fast Integer Multipliers
  [Abstract]
• 11/30/18
  Cuong Chau will talk: A Review of the Self-Timed Circuit Verification Framework
  [Abstract] [Slides]
• 11/16/18
  General Roundtable
• 10/26/18
  There will be two parts.
  • In the first hour:
    Mihir Mehta will practice a talk for the upcoming ACL2 Workshop: "Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32".
    [Abstract] [Slides]
  • Then:
    We will have a General Roundtable.
• 9/21/18
  Cuong Chau will talk: "An Update on Self-Timed Circuit Verification".
  [Abstract] [Slides]
• 5/4/18
  This will be the final meeting of the semester.
  There will be two talks.
  1. Marijn Heule will talk: "On Propositional Proofs for the Chromatic Number of the Plane."
  2. Matt Kaufmann will give a brief, informal introduction to make-event.
     [Abstract] [Demo input] [Demo log]
• 4/27/18
  Ebele Esimai will talk: "A short review of the HexNet model in ACL2".
  [Abstract] [Slides]
• 4/20/18
  There will be a General Roundtable.
  But first:
  Cuong Chau will complete his talk from last time: "A Tutorial on the ACL2 Proof of Self-Timed Circuits".
  [Abstract]
  [Note: Demo file is in the community books, in books/projects/async/fifo/queue2.lisp.]
• 4/13/18
  Cuong Chau will talk: "A Tutorial on the ACL2 Proof of Self-Timed Circuits".
  [Abstract]
  [Note: Demo file is in the community books, in books/projects/async/fifo/queue2.lisp.]
• 4/06/18
  Mihir Mehta will speak: "Verifying the FAT32 filesystem with ACL2".
  [Abstract] [Slides]
• 3/30/18
  J Moore will speak: "The Edinburgh Pure Lisp Theorem Prover in ACL2".
  [Abstract] [Slides] [Website]
• 3/23/18
  Cuong Chau will speak: "Modeling and Verifying Asynchronous Circuits Using the DE System".
  [Abstract] [Slides]
• 3/9/18
  Benjamin Kiesl (TU Wien) will speak: "A Unifying Principle for Clause-Elimination in First-Order Logic".
  [Abstract] [Slides]
• 3/2/18
  Marijn Heule will speak: "PRuning Through Satisfaction".
  [Abstract] [Slides]
• 2/27/18
  Judy Altoyan will speak: "UML Class Diagram Equivalence".
  [Abstract]
  Slides [PDF] [PPT]
  NOTE: This seminar will be on Tuesday and a bit earlier than usual: 9:15 am to 10:45 am.
  
• 2/13/18
  Ebele Esimai will talk: "Modeling HexNet in ACL2"
  NOTE: This seminar will be a bit earlier than usual: 9:30 am to 11:00 am.
  [Abstract] [Slides]
• 2/6/18
  Mertcan Temel will talk: "A Self-Timed Radix-2 FFT Design".
  [Abstract] [Slides]
• 1/26/18
  General roundtable
• 12/8/17
  General Roundtable
• 11/17/17
  Ebele Esimai will speak: "Modeling HexNet in ACL2"
  [Abstract]
  Slides [PDF] [PowerPoint]
• 11/10/17
  Mihir Mehta will give a reprise of his October 27 talk.
  [Abstract]
  [Slides]
• 11/3/17
  Mertcan Temel will talk: "DFT and FFT implementations and proofs using ACL2".
  [Abstract]
  [Slides]
• 10/27/17
  Mihir Mehta will talk: "Verifying filesystems in ACL2"
  [Abstract]
• 10/20/17
  Cuong Chau, "A Framework for Asynchronous Circuit Modeling and Verification in ACL2".
  (This is a follow-up to his previous talk asynchronous circuit modeling and will begin with a brief review.)
  [Abstract]
  [Slides]
• 9/22/17
  Cuong Chau will talk
  [Abstract] [Slides]
• 9/15/17
  Marijn Heule will speak on joint work with Benjamin Kiesl and Armin Biere: "Short Proofs Without New Variables", a paper that won the Best Paper award at at CADE-26 (2017).
  [Abstract] [PDF] [DOI] [Slides]
• 9/8/17
  General roundtable
• 5/19/17
  Benjamin Kiesl, visiting from Vienna University of Technology, will talk: "On Proofs for SAT and QBF".
  [Abstract] [Slides]
• 5/12/17
  General roundtable
• 5/5/17
  Sol Swords will talk: "Term-level Reasoning in Support of Bit-blasting"
  [Abstract] [Slides]
• 4/28/17
  Mihir Mehta will talk: "Verifying filesystems in ACL2"
  [Abstract] [Slides]
• 4/14/17
  General roundtable
• 3/31/17
  Warren Hunt will talk: "The CLRAT Parser".
  [Abstract]
• 3/24/17
  Cuong Chau will continue his 3/10/17 talk on "Modeling and Verifying Self-Timed Circuits."
• 3/10/17
  Cuong Chau will talk: "Modeling and Verifying Self-Timed Circuits Using an Asynchronous Extension of the DE System".
  [Abstract]
  
• 3/3/17
  Ben Selfridge will talk: "An ACL2 Mechanization of an Axiomatic Framework for Weak Memory".
  [Abstract]
  
• 2/24/17
  (NOTE later start time!) Marijn Heule will talk from 11:00 to 12:00: "Everything's Bigger in Texas: The Largest Math Proof Ever".
  [Abstract]
  Note: Local folks will first meet 10:05 to 10:50 for GradFest.
• 2/17/17
  Benjamin Kiesl, visiting from Vienna University of Technology, will talk: "Local Redundancy in SAT: Generalizations of Blocked Clauses".
  [Abstract] [Slides]
• 2/10/17
  General Roundtable
• 2/3/17
  Matt Kaufmann (in collaboration with Marijn J.H. Heule Warren Hunt, Jr.) will talk: "Development of a Verified, Efficient Checker for SAT Proofs".
  [Abstract] [Slides]
• 1/27/17
  Cuong Chau will talk. Title: "A DE Verification Framework for Asynchronous Circuit Verification".
  [Abstract] [Slides]
• 1/20/17
  Waqar Ahmed, PhD student visiting UT CS from the School of Electrical Engineering and Computer Science of National University of Sciences and Technology (NUST), Pakistan, will speak. Title: "Formal Dependability Analysis using Theorem Proving".
  [Abstract] [Slides]
• 12/16/16
  General roundtable
• 12/09/16
  Mihir Mehta will continue from where he left off last week.
  [Supporting materials]
• 12/02/16
  Mihir Mehta will give an introduction to the Coq prover, with a focus on induction proofs and modeling programming languages.
  [Supporting materials]
• 11/04/16
  General roundtable
• 10/21/16
  Shilpi Goel will give a practice talk for her Ph.D. Final Oral Defense: "Formal Verification of Application and System Programs Based on a Validated x86 ISA Model".
  [Abstract]
• 10/14/16
  Matt Kaufmann will talk on joint work with J Moore, "Improving Eliminate-Irrelevance for ACL2".
  [Abstract] [Slides (no pauses)] [Slides (with pauses)]
• 9/30/16
  No meeting
• 9/23/16
  Cuong Chau will talk: "An Overview of the DE Hardware Description Language and Its Application in Formal Verification of the FM9001 Microprocessor."
  [Abstract] [Slides]
• 9/16/16
  Ben Selfridge will talk: "Proving Correctness of a Simple Microprocessor Pipeline".
  [Abstract]
• 9/09/16
  Marijn Heule will talk: "Everything's Bigger in Texas: The Largest Math Proof Ever"
  [Abstract] [Slides]
• 9/02/16
  General roundtable
• 05/03/16
  There will be two talks.
  • Matt Kaufmann will talk about a tool for simplifying ACL2 definitions.
    [Abstract] [Slides (no pauses)] [Slides (with pauses)]
  • J Moore will give a short talk about his recent trip to Copan, Honduras, and Mayan hieroglyphs. This second talk has nothing to do with ACL2.
    [Information on source material]
• 4/26/16
  The group will meet 10am to 1pm (note unusual time) to visit with Tony Hoare.
  TALKS
• 4/19/16
  There will be two short talks.
  
  • Cuong Chau will talk: "Modeling Asynchronous Circuits in ACL2 Using the Link-Joint Interface".
    [Abstract] [Slides]
  • Nathan Wetzler will talk about the interviewing process.
• 4/12/16
  General roundtable.
• 4/5/16
  Marijn Heule will talk on his paper: "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer."
  [Abstract] [Slides]
• 3/29/16
  Jared Davis will talk about his development of a fast way to evaluate certain big integer expressions (which might some day be derived from hardware descriptions).
  [Abstract] [Slides]
• 3/22/16
  General roundtable.
• 3/8/16
  Matt Kaufmann will talk: "Cons-with-hint: An ACL2 development case study".
  [Abstract]
  [Notes] (text file)
• 3/1/16
  Shilpi Goel will talk: "Symbolic Simulation of x86-64 Instructions Using Congruence-Based Rewriting: A Failed but Interesting Experiment on the x86isa Model".
  [Abstract] [Slides] [Demo]
• 2/23/16
  Keshav Kini will present on the paper "A Graphical Model for Context-Free Grammar Parsing" by Keshav Pingali and Gianfranco Bilardi.
  Talk materials:
  • notes.org (slides for Emacs org-mode)
  • fig1.png (first figure for the slides above)
  • fig2.png (secondfigure for the slides above)
  • 2016-02-22-gfg.tar.xz (tarball for the materials listed above)
• 2/16/16
  J Moore will continue his series of talks (see below).
• 2/9/16
  J Moore will continue his series of talks (see below).
• 2/2/16
  General roundtable
• 1/26/16, 2/2/16 (tentative), 2/9/16
  J Moore will give a series of talks on extending ACL2 with loop and (a version of) apply.
  Abstract
  Slides and other supporting materials.
• 1/19/16
  Mihir Mehta will talk on the paper Flow-Sensitive Points-to Analysis with Term and Set Constraints by Foster, Fahndrich, and Aiken.
  Slides (pdf)
• 12/14/15
  General roundtable
• 11/30/15
  General roundtable
• 11/16/15
  Rob Sumners will talk: "Reducing Fair Stuttering Refinements of Transaction Systems".
  Abstract
  Slides
• 11/9/15
  Cuong Chau will talk about work he is doing with Marijn Heule: "Computing Unavoidable Subgraphs Using SAT Solvers".
  Abstract
  Slides
• 11/2/15
  Marijn Heule will talk: "Expressing Symmetry Breaking in Propositional Proofs".
  Abstract
  Slides
• 10/26/15
  Shilpi Goel will finish the talk she began last week.
  Then we will have a general roundtable.
• 10/19/15
  Two talks:
  • Ben Selfridge will complete his talk from a week earlier
    (see links to abstract and slides below).
  • Shilpi Goel will talk: "Reasoning about copyData: Yet Another Account of a Proof of Correctness of an x86 Machine-Code Program".
    Abstract
    Slides
• 10/12/15
  Ben Selfridge will talk: "Verifying Cache Coherence in ACL2".
  Abstract
  Slides [PDF] [Keynote (gzipped directory)]
  NOTE: Ben will give only part of his talk. The seminar will adjourn around 10:50 in order to see David Patterson's talk downstairs. Ben will complete his talk next week.
• 10/5/15
  J Moore will talk on "Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors" and/or on his current work pertaining to the Common Lisp LOOP macro. (The audience can weigh in on what he'll discuss.)
• 9/21/15
  General roundtable
• 5/19/15
  Matt Kaufmann will give an introductory ACL2 talk targeted at logicians: "ACL2: Implementation of a Computational Logic"
  Abstract
  Slides (current)
  Slides (as presented in seminar)
• 5/12/15
  General roundtable
  NOTE that we are moving back to the old time -- 10:00 am to noon -- in the usual seminar room (GDC 7.808).
• 4/28/15
  Ben Selfridge will practice his RPE talk: "An ACL2 Mechanization of an Axiomatic Framework for Weak Memory".
  Abstract
  Slides (from subsequent RPE talk)
• 4/21/15
  Shilpi Goel will practice her Ph.D. proposal talk: "Analysis of x86 Application and System Programs via Machine-Code Verification"
  Abstract
• 4/14/15
  Cuong Chau will talk: "Fourier Coefficient Formalization in ACL2(r)".
  Abstract
  Slides
• 4/13/15 (special Monday meeting at 10:00 am)
  Nathan Wetzler's dissertation defense:
  "Efficient, Mechanically-Verified Validation of Satisfiability Solvers"
  10:00 am to noon in the usual seminar room (GDC 7.808).
  Abstract
• 4/7/15
  The seminar will be split in halves (though the first "half" will be somewhat longer):
  • Nathan Wetzler will practice his dissertation defense: "Efficient, Mechanically-Verified Validation of Satisfiability Solvers".
    Abstract
  • We will have a general roundtable.
• 3/31/15
  Keshav Kini will complete the talk he began last week.
  (Last week, he got through the node accessible from the link above that is entitled "Brief demo of Coq".)
  Note "new" time: 9:00 am - 10:45 am.
• 3/24/15
  Keshav Kini will give a talk on the paper "Implementing and reasoning about hash-consed data structures in Coq" by Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux.
  Talk notes: If you bring these up in Emacs, they should come up in "org-mode"; then SHIFT-TAB will cycle through from the outline, to more, to the full notes.
  (For more about org-mode, see orgmode.org.)
• 3/3/15
  Shilpi Goel will talk: "Reasoning about Paging Data Structure Walks on x86-64 Machines".
  Abstract
  Slides
• 2/17/15
  Marijn Heule will talk: "AVATAR: A SAT-based Architecture for First-Order Theorem-Provers".
  Abstract
  Slides
• 2/10/15
  Cuong Chau will talk: "Mechanized Proof of the Orthogonality Relations of the Trigonometric Functions in ACL2(r) Using Non-Standard Analysis".
  Abstract
  Slides
• 2/3/15
  General roundtable
  Note: There will be an extra meeting on 2/3. Matt Kaufmann will give an informal introduction to ACL2(r) and non-standard analysis from 4:00 till about 5:30, as background for next week's talk.
  Talk materials
• 1/27/15
  Nathan Wetzler will talk: "farray: Field-addressable Arrays in ACL2".
  Abstract
  Slides (as a Lisp file)
  Figure referenced from slides
• 1/20/15
  Ben Selfridge will talk: "x86-TSO in ACL2: Current Status and Future Directions"
  Abstract
  
• 12/2/14
  General roundtable (last meeting of the semester)
• 11/18/14
  Matt Kaufmann will talk about the ACL2 "toothbrush" capability, for creating ACL2 applications with a small-ish memory footprint.
  Abstract
  Talk notes
• 11/4/14
  General roundtable
• 10/28/14
  Warren Hunt will talk: "Implementing AES and DES in ACL2".
  Abstract
• 10/14/14
  Shilpi Goel will talk: "Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls."
  Abstract
  Slides (pdf)
  After Shilpi's talk there will be an extended group discussion about progress towards booting FreeBSD on the x86 model. Shilpi might also go over the new model in some detail, in particular talking a bit about the new style.
• 10/7/14
  Marijn Heule will talk: "A Unified Proof System for QBF Preprocessing."
  Abstract
  
• 9/30/14
  J Moore will talk: "Some Ideas about Managing State in Code Proofs".
  Abstract
  
• 9/16/14
  Warren Hunt will give a preliminary version of a talk he plans to present later this month at a DARPA PI meeting: "Verification and Analysis Tools for X86 Binary Programs".
  Before Warren's presentation, there will be brief discussions of using git and/or magit for ACL2 book development by Matt Kaufmann and Nathan Wetzler, respectively.
  Matt's new :doc topic: git-quick-start. Improvements would be welcome!
• 9/9/14
  General roundtable
• 5/16/14
  There will be practice talks for summer conferences:
  • Matt Kaufmann will talk on a paper by
    J Moore: "Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete".
    [Abstract] [Slides (pdf)]
  • Marijn Heule will talk: "A Unified Proof System for QBF Preprocessing".
    [Abstract]
  • Nathan Wetzler will present a short talk for his SAT 2014 Tool Paper entitled "DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs" (joint work with Marijn Heule and Warren Hunt, Jr.).
    [Abstract]
• 5/02/14
  We'll start with a brief general roundtable, until about 10:30.
  Then, Nathan Wetzler will discuss a utility (joint work with Matt Kaufmann), remove-hyps, for automatically removing unnecessary hypotheses from a defthm event. He will also discuss its implementation, as a way to introduce the use of make-event for writing utilities.
  Slides (in plain text)
  Example
• 4/17/14 (note Thursday date; but the time is as usual, 10:00 - 11:45)
  Daniel Poetzl of the University of Oxford will talk: "Testing GPU Memory Models".
  Abstract
  Slides (pdf)
• 4/4/14
  General roundtable.
  But first (till 10:45):
  Cuong Chau will discuss the example (joint work with Matt Kaufmann) worked in the community book, books/demos/gl-and-use-example.lisp, showing how to obtain general theorems from special cases that are proved with GL.
  Slides for Cuong's talk
• 3/14/14
  Matt Kaufmann will talk on joint work with J Moore: "Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4".
  Abstract
  Preprint (pdf) as of 3/24/2014
• 3/7/14
  Soumava Ghosh will talk: "Executing user mode programs that perform IO on the x86 model".
  Slides
  Agenda:
  • Overview of programs that perform IO
  • Linking, loading and the x86 model
  • Converting libc-linked-programs to non-libc-linked-programs
  • Interpreting and loading a binary on the x86 model
  • Demo
  Also, Marijn Heule will report on the most recent PI meeting for the DARPA CRASH project.
• 2/28/14
  Ben Selfridge will talk: "An ACL2 Mechanization of an Axiomatic Weak Memory Model".
  Abstract
  Slides
  Shell log (using input file talk.txt)
  Supporting Materials [as .zip file] [as directory]
  
• 2/21/14
  GDC 7N folks meet at 10:00, to prepare for Grad Fest from 11:15 to 12:30
• 2/14/14
  General roundtable
• 2/3/14
  Jade Alglave of University College London will give a tutorial on weak memory (note Monday date) at the usual time, 10:00 - 11:45.
  Abstract
  Slides
  
• 12/6/13
  Shilpi Goel will talk on x86 code verification.
  Note later start time: the seminar on 12/6 will take place 11:00 to noon (or maybe a bit later).
• 12/2/13
  Prof. Mike Ernst of the University of Washington will speak: "Verification games: Making software verification fun".
  Abstract
  Slides [PDF] [PPT]
• 11/8/13,
  11/15/13,
  11/22/13
  J Moore will give a mini-course on code verification using ACL2.
  A gzipped tarball, distribution.tgz, contains all the materials below.
  Slides and ACL2 events from each talk:
  
  • Lecture 1 (Nov. 08) [slides] [ACL2 events] [session log]
    
  • Lecture 2 (Nov. 15) [slides] [ACL2 events] [session log]
    Supporting books for Lecture 2 (added after 11/16/2013 to community books directory models/jvm/m1/):
    • m1-with-stobj.lisp
    • m1-with-stobj-clock-example.lisp
  • Lecture 3 (Nov. 22) [slides] [ACL2 events] [session log]
    Supporting books for Lecture 3:
    • m1-with-stobj-defspec.lisp
    • enumerate.lisp
• 11/1/13
  We'll start with a short demo by Matt Kaufmann of the new Emacs-based ACL2-Doc browsing tool.
  Next we'll have a general roundtable.
  If time remains, Matt will go through some of the ACL2 features discussed in the documentation topic, ADVANCED-FEATURES.
• 10/18/13
  Nathan Wetzler will present his dissertation proposal: "Mechanically-Verified Validation of Satisfiability Solvers" (supervisors Warren Hunt, Jr. and Marijn Heule).
  Abstract
  Slides [Keynote] [PDF]
• 10/11/13
  Marijn Heule will talk about joint work with Warren Hunt and Nathan Wetzler (to appear in FMCAD 2013), "Trimming while Checking Clausal Proofs".
  Abstract
  [Slides [pdf]
  
• 10/4/13
  David Russinoff will talk about the rtl/rel9 library, which includes definitions and theorems for reasoning about bit vectors and floating-point operations.
• 9/27/13
  Ben Selfridge will discuss work he did this summer to capture the semantics of Kestrel's language.
  [Supporting materials]
• 9/20/13
  Jared Davis will talk about the xdoc documentation system for ACL2 and its libraries, and more generally, the future of ACL2 documentation.
  [Slides]
• 9/13/13
  General roundtable, followed -- time permitting -- by a demo, given by Shilpi Goel, that shows how to run a program on the evolving x86 model being developed by her, Warren Hunt, and our group.
• 6/19/13
  NOTE: Meeting will start at 10:00 am.
  David Rager and Nathan Wetzler will practice their ITP talks.
  • David Rager (joint work with Warren Hunt and Matt Kaufmann) "A Parallelized Theorem Prover for a Logic with Parallel Execution"
    Abstract
  • Nathan Wetzler (joint work with Marijn Heule and Warren Hunt): "Mechanical Verification of SAT Refutations with Extended Resolution"
    Abstract
• 5/28/13
  NOTE: meeting starts at 4:00 pm.
  J Moore will talk on his "codewalker" tool.
  Abstract
• 5/14/13
  Shilpi Goel will talk on her joint work with Warren Hunt (to be presented later in the month at VSTTE): "Automated Code Proofs on a Formal Model of the X86".
• 4/30/13
  There will be two talks:
  • Marijn Heule (joint work with Warren Hunt and Nathan Wetzler):
    "Efficient and Verified Checking of Unsatisfiability Proofs".
    [Abstract]
  • Warren Hunt (joint work with Nathalie Beavers, Soumava Ghosh, Shilpi Goel, Marijn J. H. Heule, Matt Kaufmann, J Strother Moore, Nathan Wetzler):
    "Formal Specification of the X86 ISA (and Using it to Verify X86 Binary Programs)"
    [Abstract]
• 4/23/13
  Soumava Ghosh will discuss his work on modeling system calls for the Y86 model. Then, Matt Kaufmann will discuss how to model the nondeterminism inherent in these system calls.
  Here are the links to the slides (original Powerpoint, and PDF format) for Soumava's half of the talk: [Powerpoint] [PDF].
  Here are links to materials for Matt's half of the talk:
  • Talk notes (really a short "paper")
  • A link to a directory of materials; you can start at the README
  • A tarball, matt.tgz, which extracts to a directory, matt/, that contains all of the above (see instructions in the README).
• 4/16/13
  General roundtable
• 4/9/13
  Sol Swords will talk about a new ACL2 library for AIGs.
  Abstract
  Talk notes
  Diagram associated with the talk
• 4/2/13
  After a short general roundtable, Shilpi Goel will give an RPE talk: "A Formal Model of the X86 ISA for Binary Program Verification".
  Abstract
  Slides
• 3/26/13
  Matt Kaufmann will talk about a new ACL2 feature: nested stobjs, that is, stobjs having fields that are stobjs (or arrays of stobjs). This will be an informal talk that briefly reviews single-threaded objects (stobjs), and then introduces nested stobjs using demos. As time allows there may be discussion of implementation issues and possible extensions. Questions will be strongly encouraged!
  Index into supporting materials
• 3/19/13
  UT group meets at 3:30 to prepare for DARPA visit.
• 3/05/13
  William Cook will talk about monads.
  Abstract
• 2/19/13
  General roundtable. Note that we will meet from 4:00 to 5:00 or 5:15.
• 2/12/13
  Ben Delaware will present his PhD proposal: "Feature Modularity in Mechanized Reasoning".
  NOTE: This will start at 3:00 pm, which is an hour earlier than our normal start time, but in the normal place, GDC 7.808.
  Abstract
• 2/5/13
  Shankar, visiting from SRI, will talk on "Programming and Proving with PVS".
  NOTE: We'll meet in our new digs on 7th Floor South of the new Gates/Dell Complex (GDC).
  Abstract
  Note: Shankar will also give a CS colloquium the same day, 11:00am-12:00pm, ACE 2.302.
• 1/22/13
  J Moore will talk: "Defining and Proving Interval Bounds for Arithmetic Functions".
  NOTE: We'll meet in MAIN 2014, as before.
  Abstract
  Talk
  Session log
• 12/4/12
  General roundtable
• 11/30/12
  There will be two ACL2 seminars this day. Please note the unusual times
  11:30am - 1:15am
  Harsh Raju Chamarthi (from Northeastern Univ., interning at Centaur Technology) will talk: "Counterexample generation in ACL2: On enumerating monadic predicates and arbitrary relations".
  Slides
  3:30pm - 5:15pm
  Marijn Heule will talk on a general framework covering all existing SAT-solving techniques.
• 11/6/12
  General roundtable
• 10/16/12
  Warren Hunt will practice his upcoming FMCAD talk on joint work with Matt Kaufmann: "A Formal Model of a Large Memory that Supports Efficient Execution".
• 10/12/12
  CP Wirth, visiting from Univ. des Saarlands and King's College London, will talk at 1:30, title: "Descente infinie, weakened admissibility conditions for recursive functions, and the automated theorem prover QUODLIBET".
  Abstract
• 10/9/12
  David Rager will present a demo on modeling network state.
  There will also be a brief (approximately 30 minute) general roundtable, time permitting.
• 10/2/12
  Shilpi Goel will talk on her joint work with Warren Hunt and Matt Kaufmann: "Applying Abstract Stobjs to Processor Modeling".
  Slides
• 9/25/12
  Ruben Gamboa of the University of Wyoming will talk: "ACL2(r) and the Completeness of the Reals".
  Abstract
• 5/7/12
  Marijn Heule will continue his talk from the last three weeks.
  Basic ACL2 implementation
  Slides
• 4/30/12
  Marijn Heule will continue his talk from the last two weeks.
  Slides
• 4/23/12
  Marijn Heule will continue his talk from last week.
  Slides
• 4/16/12
  Marijn Heule, visiting researcher at UT CS for the next year, will give an introductory talk about the state of the art in SAT solving techniques.
  Slides
• 4/9/12
  General roundtable
• 4/2/12
  Nathan Wetzler will continue last week's talk about quantification in ACL2, discussing Dave Greve's paper on quantifier automation.
  Slides for both last week and this week (pdf)
• 3/26/12
  Nathan Wetzler will talk about quantification in ACL2: basic usage, reasoning, and (via a paper from Dave Greve) automation.
  Slides for both this week and next week (pdf)
• 3/19/12
  J Moore will talk: "The Turing Completeness of M1".
  Abstract
• 3/05/12
  General roundtable.
• 2/20/12
  Robert Krug will talk about his work modeling the x86 processor. The talk will include some details of his modeling effort, but will focus on what he wants from such a model and what he hopes to use it for.
• 2/6/12
  Warren Hunt and Matt Kaufmann will discuss their evolving x86 ISA modeling effort using ACL2.
• 1/30/12
  General roundtable
• 12/12/11
  NOTE ONE-TIME ONLY TIME CHANGE: 3:00pm -4:15pm. Nirav Dave and Jonathan Woodruff, of the SRI/Cambridge(UK) team from the DARPA CRASH program, will give an overview of their project, discussing their hardware/software co-design approach and Bluespec verification work.
• 12/8/11
  General roundtable (last meeting until Feb. 1)
• 12/1/11
  J Moore will talk about his proof, with Erik Toibazarov, of the Boyer-Moore fast string searching algorithm.
• 11/17/11
  General Roundtable
• 11/10/11
  We discussed VSTTE 2012 challenge problems and corresponding solutions.
• 10/20/11
  Jared Davis will talk: "Record-like STOBJs"
  Abstract
• 10/13/11
  General Roundtable
• 10/6/11
  We'll start with a brief general roundtable. Then
  Nathan Wetzler will talk: "Existence of simple paths in ACL2".
  Abstract
• 9/29/11
  Anna Slobodova will continue her talk from last week (a revised version of her MEMOCODE 2011 talk).
  Abstract
  MEMOCODE 2011 Slides
  
• 9/22/11
  Anna Slobodova will give a revised version of her MEMOCODE 2011 talk.
  Abstract
  MEMOCODE 2011 Slides
  
• 9/15/11
  Shilpi Goel will talk: "A Formal Analysis Of Error Detecting Codes Using ACL2 (A Work In Progress)"
  Abstract
  Slides
• 9/8/11
  Nathan Wetzler will talk: "Using defattach for execution of constrained functions"
  Abstract
  Talk notes
  Shell log
• 9/1/11
  General roundtable
• 6/15/11
  Ian Wehrman will talk on his work toward a program logic for local reasoning about racy concurrent programs executing on a weak, x86-like memory model.
  Abstract
  Corresponding paper
• 6/1/11
  General roundtable
• 4/27/11
  J Moore will talk: "Reasoning about Y86 Machine Code".
  Abstract
  Slides
  Session Log
• 4/20/11
  Roy McCasland from Edinburgh will spend 15 or 20 minutes bringing us up to date on his work. Then Matt Kaufmann will discuss some topics left over from last week (but will try to make the talk reasonably self-contained), including the use of two certification runs to avoid trust tags and probably touching on make-event and defattach.
• 4/13/11
  Matt Kaufmann will talk about a framework for verified use of an external AIG+SAT solver with ACL2.
  Abstract
  Supporting files including talk notes (talk.txt) and shell log (log.txt)
• 4/6/11
  General roundtable
• 3/30/11
  (Original plans changed....)
• 3/23/11
  David Rager will talk about a futures library and parallelism abstractions for a functional subset of Lisp.
• 3/9/11
  General roundtable
• 2/23/11
  J Moore will talk on "A Datatype Manager for ACL2 -- A Work in Progress".
  Abstract
  Slides
  Session log
• 2/16/11
  Sandip Ray will give an overview of his research.
  Abstract
• 2/9/11
  General roundtable. Also, we'll talk a bit about VSTTE 2010 Challenges.
• 2/1/11 (Tuesday)
  Peter Sewell (Univ. of Cambridge) will talk from about 12:30 till 2:00. Note the unusual time and day. See:
  Abstract
• 1/19/11
  General roundtable, and discussion of future meetings
• 11/17/10
  Dave Greve (visiting from Rockwell Collins) will give a talk entitled "Efficient Type Reasoning in ACL2". He will describe some of the challenges of compositional type reasoning and propose a structured approach for reasoning about conjunctive, disjunctive and structural types.
• 11/10/10
  Ben Delaware will give a talk on his application of Coq to programming language semantics.
  Slides
• 10/27/10
  Graduate student presentations
  • Robert Krug
  • David Rager
  • Oswaldo Olivo
  • Ian Wehrman
  • Nathan Wetzler
• 10/13/10
  Instead of seminar meeting:
  UT CS Colloquium, 4pm, ACES 2.302
  Thomas Ball/Microsoft Research (http://research.microsoft.com/~tball/)
  Practical Parallel and Concurrent Programming: Performance and Correctness on the Multi-core Computer with .NET 4 (http://research.microsoft.com/ppcp/)
• 10/6/10
  Jun Sawada (IBM Austin Research Laboratory, Austin) will talk: "Automatic Verification of Estimate Functions with Polynomial of Bounded Functions".
• 5/19/10
  Robert Krug will give an introduction to temporal logic.
  Abstract
  Slides
• 5/12/10
  Matt Kaufmann will talk about some changes to ACL2 coming in the next release, which may take place within the next month.
  Talk materials
• 5/05/10
  General roundtable
• 4/21/10
  J Moore will talk on three "random" topics: a particular guard verification, a heuristic improvement, and (time permitting) a little pre-history going back to Edinburgh in 1971.
  Abstract
  Talk notes
  Notes on modifying ACL2 source code, and on adding books for proving termination and guards of ACL2 system functions
• 4/14/10
  Bill Young will lead a discussion on how best to proceed on an NSF-funded grant to investigate the verification of a hypervisor.
• 4/07/10
  General roundtable
• 3/31/10
  Anna Slobodova will discuss her use of ACL2 in verifying an integer multiplier at Centaur.
• 3/24/10
  Roy McCasland will be visiting from the University of Edinburgh, and will give a talk entitled "Automated Theorem Discovery".
  Abstract
• 3/03/10
  General roundtable
• 2/17/10
  J Moore will solicit feedback on some tutorial materials about The Method.
  Here is a pre-release of the tutorial (which is part of the current development snapshot of the ACL2 documentation); please send comments to J Moore.
• 2/10/10
  No meeting
• 2/03/10
  Matt Kaufmann will talk about the design of a defattach event for supporting execution of constrained functions, sound modification of system code, and program refinement.
  Slides [pdf]
• 1/27/10
  Rob Sumners will give an overview of his KAS rewriter, discussing some applications and the ongoing effort to prove it sound.
  Slides [pdf]
• 1/20/10
  In addition to a brief general roundtable, Sol Swords will demo some utilities developed by him and Jared Davis.
  Slides [pdf]
  Demo Script
• 12/09/09
  Robert Krug will talk about verifying simple routing protocols. Lessons will be drawn from earlier work, but this talk will focus on a plan of attack for work over the semester break. Feedback on this plan will be appreciated. Paths, routes, validity, and visibility will all be formally defined. Dijkstra's algorithm, link- state protocols, and distance vector protocols will all be discussed.
• 12/2/09
  After a brief general roundtable, Matt Kaufmann will talk on the paper, "Using Yices as an automated solver in Isabelle/HOL", by Levent Erkök and John Matthews. Yices is an SMT solver and Isabelle/HOL is a general-purpose proof assistant; it would be cool to see such a connection in use for ACL2.
  Slides [PDF] (from Erkök and Matthews)
  Additional reading: User Guide [PDF] (from Erkök and Matthews)
• 11/11/09
  Ian Wehrman will talk at 10:00 am in Warren Hunt's office on the 20th floor of the Tower (note the change in time and place).
  Abstract
  Slides [PDF]
• 11/4/09
  General roundtable
• 10/28/09
  Matt Kaufmann will talk about the ACL2 logical world and will demonstrate how to navigate the ACL2 source code.
  Abstract
  Shell log from the seminar
• 10/21/09
  Alan Dunn will talk about network protocol verification.
  Abstract
• 10/14/09
  Robert Krug will talk about his mini C interpreter. This work is a small first step towards a possible more fully featured C interpreter.
  [Abstract]
  
• 10/7/09
  General roundtable
• 9/30/09
  Jared Davis will talk about an idea for allowing ordinary ACL2 functions, which are "applicative" so that you can reason about them, to make use of more efficient programming constructs such as arrays, hash tables, parallelism, destructive updates, and so on, in a nice way, without the syntactic restrictions of stobjs, etc.
  [Slides]
  [Gzipped tar file of directory of supporting materials]
  [Directory of supporting materials]
• 9/23/09
  Sol Swords will speak about writing a clause processor that performs efficient symbolic evaluation.
  [Slides]
• 9/16/09
  Jared Davis will talk on his Milawa system, a verified stack of proof-checkers that provides a verified theorem prover.
  [Abstract]
• 9/9/09
  Alan Dunn will will discuss Carl Pixley's 1992 paper "A theory and implementation of sequential hardware equivalence".
  [Abstract]
• 9/2/09
  General roundtable (where we discuss our technical activities over the summer)
• 5/6/09
  General roundtable (last meeting till the fall)
• 4/29/09
  Ian Johnson will give an introduction to SMT solvers.
  [Slides] [Correponding paper]
• 4/22/09
  Mark Reitblatt will talk about joint work with Matt Kaufmann and Jacob Kornerup on: ``Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover.''
  [Abstract] [Slides]
• 4/15/09
  Matt Kaufmann will talk about what's new in ACL2 Version 3.5. The original notes have been updated and appear on the ACL2 2009 Workshop program page.
  
• 4/8/09
  Warren Hunt and Sandip Ray will provide an overview of some recent work on the use of ACL2 in analog/mixed-signal and post-silicon verification. The presentation is two parts: an introduction to post-silicon verification and a practice for the talk that they are going to give at the SRC verification review on April 15.
• 4/1/09
  General roundtable. Also, J Moore will talk for about 20 minutes on his experiences in the 70s with space flight software, and David Rager will talk for up to 10 minutes about his experience at the Lisp conference from which he recently returned.
• 3/25/09
  Leo Freitas (Senior Research Associate, Univ. of York, UK) will talk: "Verification Grand Challenge: open problems; and experiences with Z/Eves, an ACL2-like prover."
  Slides
• 3/11/09
  David Rager will talk about implementing a parallelism library for a functional subset of Lisp.
  Here is a page with links to the relevant paper and slides, presented at the 2009 International LISP Conference.
• 3/18/09
  No meeting (Spring break)
• 3/4/09
  We'll start with a general roundtable of about a half hour, to get a short update on what each person has been doing. Then Warren Hunt will talk about ACL2h, the HONS/memoization/fast-alist extension to ACL2. If there is extra time he may talk a bit on the topic of post-silicon verification.
  [Slides]
• 2/25/09
  First, Jared Davis completed his talk from the preceding week. Then, he gave a short talk on his defsort book.
  
• 2/18/09
  Jared Davis will discuss his Verilog translator written in ACL2h.
  [Abstract]
• 2/11/09
  Sol Swords will talk about GL, a framework for proving ACL2 theorems using BDD-based symbolic simulation.
  [Abstract] [Slides] [Demo]
• 2/4/09
  Robert Krug will present a formally verified statement of the correctness of Centaur's floating point addition unit with respect to the IEEE specification. If time permits, he will also talk about some of the changes to the arithmetic-4 books suggested by this work.
• 1/28/09
  Gabriel Infante-Lopez will talk about his development of techniques for evaluating lemma generators.
• 1/21/09
  Extended roundtable
• 12/10/08
  Sol Swords will talk about modern SAT solver algorithms.
  Slides
• 12/3/08
  Extended roundtable
• 11/5/08
  Jared Davis will talk about his recent improvements to Boyer and Hunt's ubdd package.
  Abstract
  Slides
• 10/22/08
  Robert Krug will give a high-level introductory talk, without ACL2 code, on the notion of hypervisor and how we might verify one, using an example (secVisor).
• 10/15/08
  Byron Cook of Microsoft Research (Cambridge, UK) will discuss his tool, Terminator, which automatically proves termination and other liveness properties of many industrial programs, in particular that device drivers do not hang the Windows operating system. He will describe how things work in the guts of the system, and he will be happy to take questions.
  NOTE! It is recommended that you attend the UT CS colloquium earlier that day also by Byron Cook, 11am to noon, ACES 2.402, title: "Proving That Software Eventually Does Something Good".
• 10/8/08
  Robert Krug will talk about his work for Centaur in proving correctness of a floating point addition spec (from Sol Swords) against the IEEE spec.
• 10/1/08
  William Cook will talk: "Strategic Programming with Model Interpretation and Partial Evaluation."
  Abstract
  Slides
• 9/24/08
  Sol Swords will talk on his formal verification work at Centaur Technology, including past and planned work.
• 9/10/08
  Jared Davis will discuss his Verilog parser written in ACL2.
  Abstract
  Slides
• 9/03/08
  Extended roundtable
• 5/14/08
  Jared Davis will give an informal Milawa talk and demo.
  Abstract
• 5/07/08
  Extended roundtable
• 4/30/08
  J Moore will talk about Paco, a highly slimmed-down version of ACL2.
• 4/23/08
  Sol Swords will give a broad overview of the ACL2-based toolflow being used to verify Centaur's floating-point addition unit. He'll also talk about how they split up the problem into tractable chunks, and if there's time, the strategies used to try to avoid BDD blowups while building the output BDDs of the model.
  Slides
• 4/16/08
  Warren Hunt will talk on the definition and verification of an ACL2 BDD package.
• 4/9/08
  Matt Kaufmann will talk about some work he has been doing on proving theorems about LabVIEW diagrams that have state. The talk, intended to be self-contained, will start by reviewing previous work described at the most recent ACL2 Workshop.
  Slides
• 4/2/08
  Extended roundtable
• 3/19/08
  We will finish discussing the NSF proposal on router verification that several of us have been preparing. We are likely to ask for feedback as we ready the proposal for its submission.
• 3/5/08
  Extended roundtable. Also, we will probably discuss a poster created by Sol Swords and others, which Bill Young will be presenting at an NSF Cyber Trust meeting March 16-18.
• 2/27/08
  We will continue last week's discussion about formalization of routing networks and their properties, towards an NSF proposal being developed by several of us.
• 2/20/08
  Warren Hunt and Sandip Ray will talk about formalization of routing networks and their properties, towards an NSF proposal being developed by several of us.
• 2/13/08
  Discussion of upcoming NSF Cyber Trust proposal.
• 2/6/08
  Extended roundtable. And, we will discuss whether we want to meet less frequently.
• 1/30/08
  Robert Krug will continue his talk from last week, about information flow and using ACL2 to prove properties about information flow.
  Supporting materials
• 1/23/08
  Robert Krug will talk about information flow and using ACL2 to prove properties about information flow.
• 1/16/08
  Matyas Sustik will talk on recent enhancements to the Boyer-Moore string searching algorithm.
  Abstract
• 12/12/07
  Qiang Zhang will demo, and talk briefly about, some formal verification tools for Java and C.
  Slides
• 12/05/07
  Extended roundtable and discussion of book distribution
  Some preliminary thoughts on book distribution
• 11/28/07
  Erik Reeber will talk about his SULFA tool, for verifying and generating counterexamples for a certain class of formulas, and will demonstrate with examples.
  Abstract
  Notes
• 11/07/07
  Extended roundtable
• 10/31/07
  Jared Davis will give a follow-up talk from his proposal.
  Abstract
• 10/24/07
  Jared Davis dissertation proposal, title: A trustworthy, extensible theorem prover. All seminar attendees are invited to attend -- this time (only) in the faculty lounge, Taylor 3.128, at the usual time (4:00 pm).
• 10/17/07
  Matt Kaufmann will demonstrate and discuss a new ACL2 feature, gag-mode, which is intended to give less verbose, more helpful feedback from the theorem prover in support of THE-METHOD.
  Notes
• 10/10/07
  John Erickson will give an introduction to rippling, a technique used for proofs by induction that has been developed by Alan Bundy's group at Edinburgh.
  Slides (PDF)
• 10/03/07
  Extended roundtable.
• 9/26/07
  Jacob Kornerup (from National Instruments) and Matt Kaufmann will talk about work in using ACL2 to verify LabVIEW programs.
  Abstract
• 9/19/07
  David Rager will present the information flow survey paper "Language-Based Information-flow Security" by Andrei Saberfeld and Andrew Myers.
  Abstract
  Slides [PDF] [PPT]
• 9/12/07
  Warren Hunt and J Moore will lead a discussion on what it takes to be a successful academic.
  Warren Hunt's slides [PS] [PDF]
  Additional notes (text)
• 9/05/07
  Chad Wellington will talk about his work in utilizing ACL2 to mechanize proofs of Orc language properties.
  Slides (PDF)
• 8/29/07
  Extended roundtable.
• 5/30/07
  Extended roundtable.
• 5/23/07
  J Moore will talk about string searching.
  Abstract
• 5/16/07
  Warren Hunt will talk about "Circuit Specification, Abstraction, and Reverse Engineering".
  Abstract
• 5/9/07
  Sandip Ray will talk about three strategies for deductive verification of deterministic sequential programs, along with their ACL2 proofs of completeness and soundness, highlighting the importance of quantification.
  Abstract
  Slides
  
• 5/2/07
  Extended roundtable. Everyone is expected to talk for a few minutes about what they have been doing in the past few weeks. Please come prepared.
• 4/25/07
  David Rager will talk about Parallel ACL2.
  Abstract
  Slides
• 4/18/07
  Sol Swords will continue last week's talk, about his implementation of Bryant's transistor-level circuit analysis method in ACL2.
  Abstract
  Slides [PDF] [ODP]
• 4/11/07
  Sol Swords will talk about his implementation of Bryant's transistor-level circuit analysis method in ACL2.
  Abstract
  Slides [PDF] [ODP]
• 3/28/07
  Jared Davis will talk about his use of tactics and tracing to port ACL2 proofs into Milawa, his proof checker for an ACL2-like logic with a small, trusted core.
  Abstract
  Slides [PDF] [ODP {includes notes}]
• 3/21/07
  Eric Smith will talk about his work verifying Java implementations of block ciphers (including AES) using ACL2 and STP, a bit-vector decision procedure.
  Slides (PowerPoint)
• 3/7/07
  John Erickson will talk about his work on induction, generalization and lemma generation.
• 2/28/07
  Warren Hunt will discuss the E hardware description language that he and Bob Boyer are developing, including its interpreter-style semantics written in ACL2.
  Abstract
• 2/21/07
  Qiang Zhang will discuss his language-independent pc-reachability analyzer.
  Abstract
• 2/14/07
  Erik Reeber will present his work on SULFA, a decidable subclass of ACL2 formulas that includes the ACL2 primitives if, car, cdr, cons, and consp, as well as a definitional principle.
  Abstract
• 2/7/07
  Robert Krug will continue last week's talk, by talking about the arithmetic library he has been developing.
• 1/31/07
  Robert Krug will talk about his recent work on an improved ACL2 arithmetic library and a couple of patches submitted for ACL2.
  Abstract
• 1/24/07
  Dave Greve, visiting from Rockwell Collins, will give an overview of the certification of the Rockwell Collins' AAMP7 and the Green Hills Integrity 178b Operating System, and will discuss associated theorems and challenges.
  Abstract
• 12/06/06
  Matt Kaufmann will discuss highlights of the new ACL2 release (Version 3.1).
  Abstract
  Briefly Annotated Release Notes
• 11/29/06
  Konrad Slind (faculty member at Univ. of Utah, co-maintainer of HOL4) will talk about formalizing functional programs in higher-order logic.
  Abstract
  Slides
• 11/22/06
  No meeting (Thanksgiving holiday imminent)
• 11/15/06
  A roundtable will probably be followed by a code walk on some aspect(s) of ACL2, led by J Moore.
  Abstract
• 11/8/06
  Julien Schmaltz, visiting from the Verisoft project, will talk on "Asynchronous Communications at the Gate Level: An Isabelle Theory by an ACL2 User".
  Abstract
• 11/1/06
  Qiang Zhang will review the paper "Verifying a Signature Architecture -- A Comparative Case Study" by David Basin et al., which reports on a case study in applying different formal methods, e.g. HOL-Z and PROMELA/Spin, and highlights that theorem proving may be neither substantially more time-consuming nor more complex than model checking.
  Abstract
• 10/25/06
  Keshav Pingali will talk on verification of distributed snapshot algorithms.
  Abstract
  Slides [PPT] [PDF]
• 10/18/06
  Matt Kaufmann will talk on some of the logical foundations of ACL2, in particular for the defchoose event.
  Abstract
  Brief Notes, used during the talk
  Detailed Notes (11 or 12 pages)
• 10/11/06
  Jared Davis will give a demo of the Isabelle theorem prover.
  Abstract
  Supporting materials (gzipped tarball)
• 10/4/06
  Robert Krug will give a talk modeled after one by Ken Thompson's ACM Turing Award paper over 20 years ago. Robert will discuss and demonstrate inserting a Trojan Horse into OpenMCL's compiler.
  Abstract
• 9/27/06
  Ian Wehrman will continue his talk from last week.
• 9/20/06
  Ian Wehrman will give a talk about automated equational theorem proving and term rewriting.
  Abstract
  Slides
• 9/13/06
  Dan Connolly of w3.org will give a talk related to the Semantic Web.
  Abstract
  Slides
• 9/6/06
  After an extended roundtable, Erik Reeber will give a short talk on Yices, an SMT (SAT Modulo Theory) solver developed at SRI.
  Abstract
• 8/23/06
  J Moore will talk on "Disjunctive Hints and Custom Keyword Hints".
  Abstract
• 8/9/06
  Matt Kaufmann will practice his upcoming invited ESCoR (Empirically Successful Computerized Reasoning) talk on "Maintaining the ACL2 Theorem Proving System". This talk will provide a view into the task of improving the ACL2 theorem prover to meet users' needs.
  Slides (final version)
• 8/2/06
  Jared Davis will talk about adding a ``computation'' rule to Milawa, the reflective proof checker he has been developing.
  Abstract
  Milawa web page (includes slides, movie, source code, and other material)
• 7/19/06
  Fadi Zaraket will speak on finite models of theories in equational logic.
  Abstract
  Slides [PPT]
• 7/05/06
  Sandip Ray will present his work, joint with J Moore, on how certain general forms of recursive defining equations can be admitted to ACL2.
  Abstract
  Slides [PDF]
  clock-to-trad.lisp
definition.lisp
contradiction.lisp
support.tar.gz [all of the above]
• 6/21/06
  Joe Hendrix will talk about his work on tree automata.
  Abstract
• 6/7/06
  Scott Doerrie from Johns Hopkins will talk about his work on formalizing and verifying properties of a capabilities based system.
  Abstract
• 5/24/06
  Sol Swords will speak on the disjoint set union-find problem and a solution he has coded up for it in ACL2 for use with transistor-level analysis.
  Abstract
• 5/17/06
  No meeting.
• 5/10/06
  Matt Kaufmann will talk about a new ACL2 feature, make-event, which provides the capability to do something like macro-expansion but with access to the ACL2 state and logical world.
  Abstract
• 5/03/06
  Ham Richards will talk about monads in functional programming.
  Abstract
  Notes
  A related tutorial
• 4/26/06
  Serita Nelesen will will present her work on representations in ACL2 of phylogenetic trees, which represent evolutionary relationships.
  Abstract
• 4/19/06
  Qiang Zhang will talk about his work on automating the verification of machine-level programs for an abstract computing machine.
  Abstract
• 4/12/06
  Eric Smith will be talking about a tool that generates an ACL2 proof of correctness from an annotated Java source program.
• 4/05/06
  Peter Dillinger will present the ACL2 development environment for Eclipse.
  Abstract
• 3/29/06
  Alex Spiridonov will continue the presentation started last week, this time focusing on the DrScheme interface for ACL2.
• 3/22/06
  Alex Spiridonov will talk about two projects that have emerged to provide an intuitive graphical interface for ACL2: ACL2 in Eclipse and ACL2 in DrScheme.
  Abstract
• 3/8/06
  Hanbing Liu will discuss his JVM-related research.
  Abstract
  Slides
• 2/28/06
  Robert Krug will talk about his work in support of the Destiny tool being developed at the NSA.
  Abstract
  Slides
  
• 2/22/06
  Sandip Ray will talk about ongoing work on the integration of assertional reasoning with operational semantics using ACL2.
  Abstract
  Slides [PDF]
• 2/15/06
  Matt Kaufmann will lead a discussion on useful features of ACL2.
  Abstract
  Script for the demo
  Shell log from the demo
• 2/8/06
  Eric Smith will present his additions to compositional cutpoint reasoning and its application to the AAMP7 microprocessor.
  Abstract
  Slides [PDF]
  Slides [remote, PPT]
• 2/1/06
  David Rager will present his work on shared-key establishment protocol JFKr.
  Abstract
  Slides
• 1/25/06
  J Moore will talk on "An Entertaining Puzzle".
  Abstract
• 11/30/05
  Prof. Shang-Ching Chou of Wichita State Univ. will talk about some of his work in automated reasoning for geometry.
  Abstract
• 11/23/05
  No seminar; it will resume next week.
• 11/16/05
  Jared Davis will present some preliminary work on developing a trustworthy and capable proof checker for an ACL2-like logic.
  Abstract
• 11/9/05
  Warren Hunt will continue last week's talk.
• 11/2/05
  Warren Hunt will discuss a hash cons implementation (by him and Bob Boyer), with new and updated slides.
  Abstract
• 10/26/05
  Extended roundtable discussion, including Matt Wilding visiting from Rockwell Collins.
• 10/19/05
  Grant Passmore will talk on his work at National Instruments involving ACL2 and LabVIEW/G.
  Abstract
  Slides
  
• 10/12/05
  Jared Davis will talk on a fast implementation of records for ACL2.
  Abstract
  Slides
  
• 10/5/05
  Robert Krug will talk about (1) How to use the arithmetic-3 library, and (2) How to use bind-free to develop a powerful library.
• 9/28/05
  Erik Reeber will be presenting the paper he and Warren Hunt wrote on the DE2 language, practicing for his presentation at CHARME next week.
  Abstract
• 9/21/05
  Sol Swords and William Cook will continue last week's talk.
• 9/14/05
  Sol Swords and William Cook will talk about their ACL2 work on the POPLMark challenge to create a system for machine-checked proofs of theorems about programming languages (subtyping and soundness for polymorphic lambda-calculi); see http://www.cis.upenn.edu/group/proj/plclub/mmm/. They will also discuss some macros for ACL2 based on ideas from Haskell.
• 9/07/05
  Extended roundtable
• 8/17/05
  Gary Byers, the leader of the OpenMCL project, will give a presentation about OpenMCL. This note will probably be updated later, but at this point it seems that the presentation will discuss (at least) the OpenMCL compiler, possible future directions for the OpenMCL project, and OpenMCL support for parallel execution.
  Slides [PDF]
• 7/27/05
  Professor Jingchao Chen from Donghua University in Shanghai will present a talk on Mizar. (Also see Journal of Formalized Mathematics.)
• 7/20/05
  David Rager will "give an update on what parallelization currently means for ACL2."
  Abstract
  Slides [PDF black and white] [PDF color]
  ACL2 and Lisp Tests [PDF]
  
• 6/15/05, Hormoz Zarnani
  Hormoz will discuss: "Verifying the Intentional Naming System."
  Abstract
  
• 5/18/05, Bill Young
  Bill will talk about "techniques for automatically `retrofitting' a detailed low-level model with abstractions that facilitate reasoning about the properties of a model."
  Abstract
  
• 5/11/05, Camm Maguire
  Camm is the lead developer for Gnu Common Lisp (GCL), and he will talk with us about GCL.
  Abstract
  
• 5/04/05, David Rager
  David will discuss parallelizing ACL2.
  Abstract and Handouts
  
• 4/27/05, Hanbing Liu
  Hanbing Liu will be discussing Abstract Interpretation.
  Abstract
  Slides
  
• 4/20/05, John Matthews
  Title: "Deeply embedding Cryptol in ACL2: A challenge problem."
  Abstract
  Slides [PDF]
  ACL2 challenge problem: Formalizing BitCryptol [Text]
• 4/13/05, Matt Kaufmann
  Continuation (to completion) of last week's talk. Time permitting, some details may be given that aren't in the notes.
• 4/06/05, Matt Kaufmann
  "Structured Theory and the Axiom of Choice."
  Abstract
  Notes
• 3/30/05
  Roundtable at the usual time and place (4pm, ACES 6.442) will be followed by:
  "The Future of Computing", Dirk Meyer, Executive VP of AMD's Computation Products Group, 5:00 p.m., ACES 2.302.
  Abstract
• 3/23/05, Carlos Pacheco
  Carlos will describe a technique that helps a test engineer select, from a large set of randomly-generated candidate test inputs, a small subset likely to reveal faults in the software under test.
  Abstract
• 3/16/05
  No seminar (spring break)
• 3/9/05, Serita Nelesen
  Serita will continue last week's talk on computational biology work based on the hash consing work that Warren Hunt presented 2/23.
  Abstract
  Slides
• 3/2/05, Serita Nelesen
  Serita will talk on about computational biology work based on the hash consing work that Warren Hunt presented last week.
  Abstract
  Slides
• 2/23/05, Warren Hunt (joint work with Bob Boyer), possibly followed by Serita Nelesen
  Warren will talk on joint work with Bob Boyer: "Function Memoization and Unique Explicit Object Representation".
  Abstract
• 2/16/05, Jared Davis
  Jared will complete last week's talk about using ACL2 as an environment for formal software development.
  Abstract
  Jared's Slides (updated from last week)
  
• 2/09/05, Jared Davis
  Jared will talk about using ACL2 as an environment for formal software development.
  Abstract
  Slides (updated from those originally presented)
• 2/02/05, Erik Reeber
  Erik will continue with the third in this series of talks.
  Slides
  Slides for preceding week (second week of series).
  Slides for week before that (first week of series).
• 1/26/05, Erik Reeber
  Erik will continue with last week's talk.
  Slides
• 1/19/05, Erik Reeber
  Erik will present his work on integrating SAT solving with ACL2.
  Abstract
  Slides
• 12/08/04, David Rager
  David will talk about pretty printing in general, term highlighting, and (new to ACL2) both term hiding and unhiding. If time he may talk about modeling security key-establishment protocols.
  Abstract
• 12/01/04, John Erickson
  John will talk about improving the automation of induction by considering example cases.
  Abstract
• 11/03/04, Jared Davis
  Jared will talk about extensions to his finite set theory library.
  Abstract
• 10/20/04, Shant Harutunian
  Shant will talk on his use of non-standard analysis to model two simple dynamic systems.
  Abstract
• 10/20/04, Qiang Zhang
  Qiang will continue with last week's talk (see below).
• 10/13/04, Qiang Zhang
  Qiang will present his work on proving the correctness of Dijkstra's shortest path algorithm.
  Abstract
  Slides
• 10/06/04, Robert Krug
  Robert will give a short presentation on ``The Limits of Mathematics,'' based on G. J. Chaitin's book of the same name.
  Abstract
• 9/29/04, no speaker
  Extended round-table discussion
• 9/22/04, Jared Davis
  "Abettor Interfacing System for ACL2."
  Jared will be presenting his work on extending the ACL2 user interface. Abettor is a client/server framework for simultaneously connecting multiple external tools to an ACL2 session. Abstract
• 9/15/04, J Moore
  J will give a presentation of exploratory work on the use of second-order pattern matching to automate functional instantiation.
  Abstract
• 9/8/04, Hanbing Liu
  Hanbing will present his work on modeling the JVM (Java Virtual Machine) and proving properties of simple Java programs via the JVM model.
  Abstract
  Slides of TPHOLs talk [PDF]
• 9/1/04, Rob Sumners
  Rob will continue with his talk of 8/18.
• 8/18/04, Rob Sumners
  Rob will give an example-driven talk about some work that he and Sandip Ray have been doing in "automating" the proof of invariants for certain types of system definitions in ACL2.
  Abstract
  Slides [PS] [PDF]
• 8/4/04, Matt Kaufmann
  Matt will talk about some issues with guards and evaluation in ACL2.
  Abstract
  Notes for First Part
  Notes for Second Part
  Notes for Third Part
• 7/21/04, Ruben Gamboa
  Ruben will talk about ACL2(r), which is his modification of ACL2 to support reasoning about real numbers through non-standard analysis. After a suitable introduction, the bulk of the talk will be devoted to the correctness of ACL2(r).
  Abstract
• 6/30/04, Erik Reeber
  Erik will be restarting his description of the DE hardware description language (previously started 5/19).
  Abstract
  Slides [pdf] [Powerpoint]
• 6/16/04, Fares Fraij
  Fares will continue last time's talk (on modelling program transformations in ACL2).
• 6/4/04, Fares Fraij
  Fares will be presenting his work on modelling program transformations in ACL2.
  Abstract
  Slides (pdf)
• 5/19/04, Erik Reeber
  Erik will describe the DE hardware description language, with a focus on the differences between DUAL-EVAL and DE.
  Abstract
• 5/05/04, Hanbing Liu
  Hanbing will present his formalization of a ring data structure in ACL2, and will briefly describe a mechanically checked proof about it.
  Abstract
• 4/28/04, Vinod Vishwanath
  Vinod will continue last week's talk about sequential simplification of hardware circuits.
  Abstract
• 4/21/04, Vinod Vishwanath
  Vinod will talk about sequential simplification of hardware circuits.
  Abstract
• 4/14/04, Julien Schmaltz
  Julien will talk about modeling and verification of ethernet protocols in ACL2.
  Abstract
• 4/07/04, Bill Young
  Bill will talk cryptographic protocols and some approaches toward proving them correct. This will focus on the work of Larry Paulson from Cambridge and his use of the Isabelle system to prove properties of protocols inductively.
• 3/31/04, Bill Young
  Bill will continue last week's talk about modeling security policies in ACL2.
  Abstract
• 3/24/04, Bill Young
  Bill will talk about modeling security policies in ACL2.
  Abstract
• 3/10/04, Anna Slobodova
  Change of room this time only to 5.116.
  Anna will talk about verification of the floating point unit of the next generation Itanium (R) processor. This will be a dry run for her presentation in DCC'2004.
  Abstract
• 3/03/04, Xiaozhou (Steve) Li
  Xiaozhou (Steve) Li will present a topology maintenance protocol for p2p networks. They are planning to verify this protocol with ACL2.
  Abstract
  Slides
  Tech report
• 2/18/04, Jared Davis
  Jared will continue last week's talk about a new finite sets implementation.
  Web page (includes slides, at 3rd bullet under "Documentation")
• 2/11/04, Jared Davis
  Jared will be talking about a new finite sets implementation, wherein the set elements are fully ordered.
• 2/04/04, J Moore
  Intended topics are as follows, time permitting:
  
  1. Discuss the ACL2 bug exposed last week by Qiang Zhang, including discussion of source function if-tautologyp.
  2. Show a resolution theorem prover in ACL2 and use it to prove a few first order theorems involving search.
  3. Explain 2nd order pattern matching (because J has been thinking about it and we've been discussing unification).
• 1/28/04, J Moore
  Resolution Theorem Proving, Part 2; possibly next week as well.
  Abstract
• 1/21/04, J Moore
  Resolution Theorem Proving, Part 1.
  Abstract
• 12/17/03, Sandip Ray
  Sandip will continue last week's talk.
• 12/10/03, Sandip Ray
  Sandip will talk on joint work with J Moore: "Proof Styles in Operational Semantics."
  Abstract
  Presentation slides
  Paper
• 12/3/03, Fares Fraij
  Fares Fraij from UTEP will talk on his proposed handling of the verification of a transformation system (namely HATS).
  Abstract
  PowerPoint slides
  Toy model (HATS-toy-model.lisp)
• 11/19/03, Julien Schmaltz
  Julien will talk about his work over the last three months on modeling, and proving theorems about, a network on a chip.
  Abstract
• 11/12/03, J Moore
  J will report on his recent trip. He will also lead a discussion to get feedback on the "Key Research Problems" section of a paper to be submitted to a special issue of the Spanish Academy of Science.
• 11/05/03, Erik Reeber
  Erik will give an informal overview of his ongoing work with DE and zChaff.
  Abstract
• 10/29/03, Sandip Ray
  Sandip will practice his Ph.D. Oral proposal talk: "Using Theorem Proving and Algorithmic Techniques for Large-Scale System Verification".
  Abstract
  Slides [PDF]
  Proposal Document
• 10/22/03, Matt Kaufmann
  Matt will talk about the ACL2 logic.
  Abstract
• 10/15/03, Matt Kaufmann
  Matt will talk about the ACL2 "to do" list. He hopes that this seminar will help us answer the following question: How much more should we do to ACL2 before releasing Version 2.8?
  Attendees are encouraged to suggest particular items from the following list for discussion at the seminar (feel free to email kaufmann@cs.utexas.edu ahead of time):
  Detailed abstract and list of "todo items".
  Copies of this list will be distributed at the seminar.
  By the way, a list of what is _already_ new for ACL2 Version 2.8 may be found at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/whats-new/talk.txt.
• 10/08/03, Robert Krug
  Robert will talk about staged simplification.
  Robert says:
  

  I will talk briefly about staged simplification. Several years ago Pete Manolios and J introduced the notion of stable-under-simplificationp to control rewriting expressions involving a large and detailed machine. Since then, I have found that there is great benefit to be derived by enabling (and subsequently disabling) nonlinear arithmetic under similar control. Both of these are related to the common strategy of examining a failed proof and giving hints at the ``checkpoints''.

• 10/01/03, Warren Hunt and Robert Krug
  Warren will give a first practice talk for his paper with Robert on nonlinear arithmetic at CHARME.
• 9/24/03, no speaker
  Extended round-table discussion
• 9/17/03, Jared Davis
  Jared will talk about a new project he is hoping to explore, involving formal verification of program transformations.
  Abstract
• 9/10/03, Julien Schmaltz
  Julien will talk about an ACL2 proof of the termination of a routing algorithm for a network on-chip architecture.
  Abstract
  Paper [PDF] [PS]
  ACL2 source files:
  • Gzipped tar file: go-to-node.tar.gz
  • Directory listing for individual files
• 9/3/03, no speaker
  Extended round-table discussion
• 8/20/03, Matyas Sustik
  Matyas will continue from last week's talk about quantifier elimination (same abstract and slides as below).
• 8/20/03, Matyas Sustik
  Matyas will talk about quantifier elimination.
  Abstract
  Also see http://www.cs.utexas.edu/users/sustik/quantifier-elimination/ for slides, papers and references.
• 8/13/03, Fares Fraij
  Fares will talk about his experiences with ACL2 from the perspective of a new user.
• 8/06/03, Robert Krug
  Robert will continue talking about how to write a library of arithmetic books.
• 7/30/03, Robert Krug
  Robert will continue talking about how to write a library of arithmetic books.
• 7/23/03, Robert Krug
  Robert will continue talking about how to write a library of arithmetic books.
• 7/16/03, Robert Krug
  How to write a library of arithmetic books.
• 7/02/03, Joe Hendrix
  An overview of Maude
  Slides [PDF] [PS]
  Maude input files:
  • fib.maude
  • graph.maude
  • meta.maude
  • nat.maude
  • path.maude
  • set.maude
• 6/25/03, Joe Hendrix
  The new Java memory models, continued
  Slides [Postscript] (same as last week's)
• 6/18/03, Joe Hendrix
  The new Java memory models
  Slides [Postscript]
• 6/11/03, Robert Krug
  Some work with ACL2 and arithmetic
  Abstract
• 6/04/03, Matyas Sustik
  Matyas will talk on his proof of Dixon's Lemma in ACL2
  Abstract
  See Matyas's home page for a link to get to the slides.
• 5/28/03, Hanbing Liu
  Hanbing will give a talk based his paper with J Moore, "Executable JVM Model for Analytical Reasoning: A Study"
  Abstract
  The paper (PS)
• 5/21/03, Matt Kaufmann
  Dealing With Prover Heuristics in ACL2: A Case Study
  Talk notes
  NOTE: This will be a short talk. Most of the meeting will consist of an extended round-table discussion, perhaps with a focus on upcoming summer projects.
• 4/30/03, Qiang Zhang
  Qiang will complete his 4/16 talk on compiler verification.
  Also, we will figure out the summer schedule.
• 4/23/03, J Moore
  J Moore will talk about about partial functions in ACL2:
  2000 ACL2 Workshop paper (P. Manoilios, J Moore) [PDF] [PS] [Supporting Materials]
• 4/16/03, Qiang Zhang
  [Qiang will talk on his work on compiler verification.]
• 4/09/03, John Erickson
  Generalizing Finite Cases
  Abstract
• 4/02/03
  No seminar, but people are encouraged to attend the following colloquium talk:
  TAY 3.128, 4:00 pm (coffee at 3:30)
  Steven M. German, IBM T.J. Watson Research Center
  Experiences in Formal Design and Verification of Cache Memory
• 3/26/03, Rob Sumners
  Continuation of preceding week's talk
  Slides [Postscript] (same as last week's)
• 3/19/03, Rob Sumners
  A New Simplifier
  Slides [Postscript]
• 3/12/03, no seminar (spring break)
• 3/05/03, Sandip Ray
  Continuation of preceding week's talk
  [See just below for slides etc.]
• 2/26/03, Sandip Ray
  Continuation of preceding week's talk
  [See just below for slides etc.]
• 2/19/03, Sandip Ray
  Continuation of preceding week's talk
  [See just below for slides etc.]
• 2/12/03, Sandip Ray
  Verification of model-checking reductions at CRL
  Abstract
  Slides [HTML]
  Slides [Postscript; printing works, but viewing may not work]
  .lisp file
  Also, Matt Kaufmann will talk briefly about recent changes in rewriting under induction.
• 1/29/03, no speaker
  Extended round-table discussion
• 1/22/03, Erik Reeber
  Review of work of Praxis Critical Systems
  Abstract
  Slides
• 1/15/03
  Extended round-table discussion.
  NOTE: If time, Matt Kaufmann will discuss:
  Proposal for attaching executable functions to logic definitions.
  Matt will also mention Avoiding infinite loops in the ACL2 rewriter.
• 12/04/02, Bill Young
  Review of "Transformation-Oriented Programming: A Development Methodology for High Assurance Software" by Victor Winter, Steve Roach, Greg Wickstrom.
  [J asked Bill to look at this to assess whether ACL2 could somehow be used in this context.]
• 11/20/02, Shant Harutunian
  Continuation of preceding week's talk (Note: slides have been further updated.)
• 11/13/02
  
  • J Moore
    Short discussion on how to structure his upcoming JVM class
    
  • Shant Harutunian
    Continuation of preceding week's talk (Note: slides have been updated.)
• 11/06/02, Shant Harutunian
  Model-Checking in Dense Real Time
  Abstract [plain text]
  Slides [PDF]
• 10/30/02, no speaker
  Extended round-table discussion
• 10/23/02, Robert Krug
  Continuation of preceding weeks' talks
• 10/16/02, Robert Krug
  Continuation of preceding week's talk
• 10/9/02, Robert Krug
  Arithmetic in ACL2
  Abstract [plain text]
• 10/2/02, Robert Krug
  ACL2 Basics
  Abstract [plain text]
• 9/25/02, Hanbing Liu
  Continuation of preceding week's talk
  Abstract [plain text]
• 9/18/02, Hanbing Liu
  Introduction to ACL2 JVM Models
  Abstract [plain text]
  Slides [PDF] [PPT]
• 9/11/02, Vinod Viswanath
  Assertion Based Verification of Hardware Circuits
  Abstract [plain text]
  Slides [PDF]
• 9/4/02
  • Robert Krug
    Brief talk on break-rewrite
  • Michael "Bogo" Bogomolny
    Paper review: "Little Engines of Proof", by N. Shankar
    Shankar's paper [PDF]
    Shankar's slides [PDF]
• 8/28/02, Matt Kaufmann
  A Tool for Simplifying Files of Definitions
  Abstract [plain text]
  Handout [plain text]