SAT 2015: 18TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
ACL2-2015 PROGRAM

Days: Thursday, October 1st Friday, October 2nd

Thursday, October 1st

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:10-10:30 Session 53
09:10
Invited Talk: Lessons Learned over 45 Years in Theorem Proving ( abstract )
10:10
A Brief Introduction to Oracle’s Use of ACL2 ( abstract )
11:00-12:30 Session 54
11:00
Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning ( abstract )
11:30
Second-Order Functions and Theorems in ACL2 ( abstract )
12:00
R1 ( abstract )
13:30-14:30 Session 55: (PANEL) Industrial Use of ACL2: Present and Future

Panelists: Jo Ebergen, Oracle
David Hardin, Rockwell Collins;
David Russinoff, Intel;
Rob Sumners, AMD;
Sol Swords, Centaur

15:00-16:15 Session 56
15:00
Fourier Series Formalization in ACL2(r) ( abstract )
15:30
Perfect Numbers in ACL2 ( abstract )
16:00
R2 ( abstract )
Friday, October 2nd

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:30 Session 58
09:00
Invited Talk: Verification in the Age of Integration ( abstract )
10:00
Extending ACL2 with SMT Solvers ( abstract )
11:00-12:30 Session 59
11:00
Reasoning about LLVM code using Codewalker ( abstract )
11:30
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States ( abstract )
12:00
Proving Skipping Refinement with ACL2s ( abstract )
13:30-15:00 Session 60
13:30
R4 ( abstract )
14:00
What's New in the Community Books ( abstract )
14:30
What's New in ACL2 ( abstract )