14th International Workshop on the
ACL2 Theorem Prover and Its Applications

Sunday, May 21: Welcome Reception
18:00 -
Welcome Reception -- food will be served
House of Anna Slobodova and Warren Hunt
2106 Ringtail Ridge, Austin, TX
[Directions from Austin Folk House]
[Directions from The Quarters at Hardin House] ]
Monday, May 22: Day 1
09:00 Welcome
  Session 1
09:10 Grant Passmore
(Aesthetic Integration)
Invited talk 2
Formal Verification of Financial Algorithms, Progress and Prospects
10:10 Shilpi Goel The x86isa Books: Features, Usage, and Future Plans
10:40 BREAK
  Session 2
11:00 John Cowles
Ruben Gamboa
The Cayley-Dickson Construction in ACL2
11:30 David Russinoff A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve
12:00 LUNCH
  Session 3
13:30 Rump Session 1
(20 minute talks)
15:15 BREAK
  Session 4
15:30 Matt Kaufmann
Sol Swords
Meta-extract: Using Existing Facts in Meta-reasoning
16:00 Alessandro Coglio
Matt Kaufmann
Eric W. Smith
A Versatile, Sound Tool for Simplifying Definitions
16:30 Rump Session 2
(20 minute talks)
End of first day's program
18:30 -
CONFERENCE DINNER Manuel's downtown
310 Congress Avenue, Austin, Texas 78701 (map)
Tuesday, May 23: Day 2
  Session 5
09:00 Glenn Henry
(Centaur Technology)
Invited talk 1
Using Mechanized Mathematics in an Organization with a Simulation-Based Mentality
10:00 Rob Sumners Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications
10:30 BREAK
  Session 6
11:00 Sol Swords Term-Level Reasoning in Support Of Bit-Blasting
11:30 Cuong Chau Extended Abstract: Formal Specification and Verification of the FM9001 Microprocessor Using the DE System
11:50 Rump Session 3
(20 minute talks)
12:10 LUNCH
  Session 7
13:30 Greg Grohoski
Invited talk 3
Verifying Oracle's SPARC Processors with ACL2
14:00 Matt Kaufmann What's new in the ACL2 system
14:30 Alessandro Coglio
Sol Swords
(and others?)
What's new in the community books
15:00 BREAK
  Session 8
15:30 Business Meeting and Discussion
16:30 Rump Session 4
(15 minute talks)
17:30 (tentative) Workshop ends