PROGRAM
15th International Workshop on the
ACL2 Theorem Prover and Its Applications
(ACL2-2018)

Notes:

• All workshop activities except the evening activities (reception Sunday, banquet Monday) will take place on the campus of the University of Texas in the Dell-Gates Complex (GDC), North Wing, Room 6.302 (Faculty Lounge). GDC is located south of 24th Street on Speedway. Visitor parking is available in the parking garages, of which the San Jacinto Garage is closest to GDC.

• Proceedings (EPTCS 280) are available online, as described here.
• An alphabetical list of participants is available.

Sunday, November 4: Welcome Reception
18:00 - 21:00 (may end a bit later)	Welcome Reception -- dinner will be served (buffet style) House of Holly Bell and Matt Kaufmann 2203 Euclid Ave., Austin, TX Usually there's plenty of nearby parking on the street; or you can take a bus from the UT campus (also see the bus website). Significant others are welcome!
Monday, November 5: Day 1
08:30	BREAKFAST
	Session 1 (chair: Matt Kaufmann)
09:00	Welcome
09:10	Sandip Ray (University of Florida at Gainesville)	Invited talk 1 Small Team, Short Ramp, Industrial-scale Problems: Some Experiments in the Practicum of Interactive Theorem Proving
10:10	Sol Swords	Incremental SAT Library Integration using Abstract Stobjs [Slides]
10:40	BREAK
	Session 2 (chair: Warren Hunt)
11:00	Mihir Mehta	Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32 [Slides]
11:30	Alessandro Coglio Shilpi Goel	Adding 32-bit Mode to the ACL2 Model of the x86 ISA [Keynote slides, with animations] [PDF slides, with simpler animations] [PDF slides, with no animations]
12:00	Alessandro Coglio	A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java [Animated PowerPoint Show file (viewable with free PowerPoint Viewer)] [PDF slides (not animated)]
12:30	LUNCH
	Session 3 (chair: Shilpi Goel)
14:00	Sol Swords (Centaur Technology)	Invited talk 2 Building Blocks for RTL Verification in ACL2 [Slides]
15:00	David Hardin Konrad Slind	Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems [Slides]
15:30	BREAK
	Session 4 (chair: Anna Slobodova)
15:50	Rob Sumners	A Toolbox for Property Checking from Simulation Using Incremental SAT (Extended Abstract) [Slides]
16:10	Rump Session talks	Rob Sumners, Analyzing Khipu in ACL2 (15 min.) [Slides] Shilpi Goel (speaker) and Mayank Manjrekar, A Formalization of an Instant Run-Off Voting Scheme (15 min.) [Slides]
16:40	BREAK
	Session 5 (chair: Alessandro Coglio)
17:00	David Greve Andrew Gacek	Trapezoidal Generalization over Linear Constraints [Slides]
17:30	Rump Session talks	David Greve, Predicate Refinement and Equivalences (20 min.) [Slides] Nathan Guermond, Graph algorithms and their specifications in ACL2 (10 min.) [Slides]
18:00	Day 1 program ends
18:30 - 21:00	CONFERENCE DINNER	Aster's Ethiopian Restaurant 2804 N Interstate 35 Austin, TX 78705 [Map from workshop] 6:30 to 9:00 (wine at 6:30; buffet at 7:00) [For those who want to hang out afterwards, one possibility is to Bennu Coffee.]
Tuesday, November 6: Day 2
08:30	BREAKFAST
	Session 1 (chair: David Russinoff)
09:00	Alastair Reid (ARM)	Invited talk 3 Creating Formal Specifications of the Arm Processor Architecture [Slides]
10:00	Ruben Gamboa John Cowles	The Fundamental Theorem of Algebra in ACL2 [Slides]
10:30	Rump Session talk	Keshav Kini, Verifying a fast SHA-256 implementation on AVR (10 min.)
10:40	BREAK
	Session 2 (chair: Ruben Gamboa)
11:00	Carl Kwan Mark Greenstreet	Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r) [Slides] (includes next talk)
11:30	Carl Kwan Mark Greenstreet	Convex Functions in ACL2(r) [Slides] (includes preceding talk)
12:00	Yan Peng Mark Greenstreet	Smtlink 2.0 [Slides]
12:30	LUNCH
	Session 3 (chair: David Rager)
14:00	Alessandro Coglio	What's New in the Community Books [Slides]
14:30	Matt Kaufmann	DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract) [Slides [Without pauses] [With pauses]]
14:50	Matt Kaufmann J Moore	What's New in the ACL2 System [Slides (not including :doc topics)] [Video (you may want to skip to the 2:29 mark; the fun starts within 15 seconds from there)]
15:20	BREAK
	Session 4 (chair: Dave Greve)
15:40	Sol Swords	Hint Orchestration Using ACL2's Simplifier [Slides]
16:10	Rump Session talks	David Russinoff, Formal Verification of Floating-Point Hardware Design: A Mathematical Approach (15 min.) [Slides] Matt Kaufmann, Preserving the Structure of Definitions After Simplification (15 min.) [Slides]
16:40	BREAK
	Session 5
17:00	Business Meeting	Tentative list of topics is here.
18:00	Workshop ends