ACL2 Theorem Proving Seminar at the University of Texas

Previous meetings (reverse order):

• 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
  Rountable 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
  [NOTE that this week only, we will be meeting in TAY 3.128 (the faculty lounge) rather than ACES, though still at the usual time.]
  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]