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 ) |
16:45-18:00 Session 57
| 16:45 | R3 ( 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 ) |
15:30-17:00 Session 61
| 15:30 | R5 ( abstract ) |
| 16:00 | Business Meeting ( abstract ) |