CADE-17
Program
David McAllester, Program Chair
Events are held in the University Center unless otherwise noted. The main events are in McConomy Auditorium, registration and breaks in the adjacent Connan Room. Lunch is downstairs in Rangos Hall. Workshops, tutorials, and system competition will be held in Wean Hall. System demonstrations will be in the break following the 10-minute system presentation in a room near McConomy Auditorium.
The banquet will be held at the Pittsburgh Golf Club, which is located adjacent to the Carnegie Mellon Campus, about a 5 minute walk away from the University Center.
| |
|
| Friday, June 16: Workshops and Tutorials | |
| 7:00-9:00 Welcome Reception, Connan Room, UC | |
| |
|
| Saturday, June 17 | |
| |
|
| 8:45 | Opening Remarks: Ulrich Furbach, President of CADE |
| 9:00 | Invited Talk: High-Level Verification Using Theorem Proving and Formalized Mathematics |
| John Harrison | |
| 10:00 | CASC Entrants' Meeting, Connan Room, UC |
| Followed by System Competition, 5th Floor Cluster, Wean Hall | |
| 10:00 | Coffee Break |
| 10:30 | Machine Instruction Syntax and Semantics in Higher Order Logic |
| Neophytos G. Michael and Andrew Appel | |
| 11:00 | Proof Generation in the Touchstone Theorem Prover |
| George C. Necula and Peter Lee | |
| 11:30 | Wellfounded Schematic Definitions |
| Konrad Slind | |
| 12:00 | Lunch |
| 1:30 | Abstract Congruence Closure and Specializations |
| Leo Bachmair and Ashish Tiwari | |
| 2:00 | A Framework for Cooperating Decision Procedures |
| Clark W. Barrett, David L. Dill, and Aaron Stump | |
| 2:30 | Modular Reasoning in Isabelle |
| Florian Kammuller | |
| 3:00 | An Infrastructure for Intertheory Reasoning |
| William Farmer | |
| 3:30 | Break |
| 4:00 | Godel's Algorithm for Class Formation |
| Johan Gijsbertus Frederik Belinfante | |
| 4:30 | Automated Proof Construction in Type Theory using Resolution |
| Marc Bezem, Dimitri Hendriks and Hans de Nivelle | |
| 5:00 | System: TPS, A Theorem Proving System for Type Theory |
| Peter B. Andrews, Matthew Bishop and Chad E. Brown | |
| 5:10 | System: The Nuprl Open Logical Environment |
| S. F. Allen, R. L. Constable, R. Eaton, C. Kreitz and L. Lorigo | |
| 5:20 | System: ARA - An Automatic Theorem Prover for Relation Algebras |
| Carsten Sinz | |
| 5:30 | End of Session |
| |
|
| Sunday June 18 | |
| |
|
| 8:45 | Invited Talk: Scalable Knowledge Representation and Reasoning Systems |
| Henry Kautz | |
| 9:45 | Coffee Break |
| 10:00 | Efficient Minimal Model Generation Using Branching Lemmas |
| Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura | |
| 10:30 | FDPLL --- A First Order Davis-Putnam-Loveland Procedure |
| Peter Baumgartner | |
| 11:00 | Rigid E-Unification Revisited |
| A. Tiwari, L. Bachmair, and H. Ruess | |
| 11:30 | Break |
| 12:00 | Excursion Buses Leave from University Center |
| 6:00 | Return from Excursion |
| 7:30 | Banquet, Pittsburgh Golf Club |
| |
|
| Monday, June 19 | |
| |
|
| 8:45 | Invited Talk: Connecting Bits with Floating-Point Numbers: |
| Model Checking and Theorem Proving in Practice | |
| Carl Seger | |
| 9:45 | Coffee Break |
| 10:15 | Reducing Model Checking of the Many to the Few |
| E. Allen Emerson and Vineet Kahlon | |
| 10:45 | Simulation Based Minimization |
| Doron Bustan and Orna Grumberg | |
| 11:15 | Rewriting for Cryptographic Protocol Verification |
| Thomas Genet and Francis Klay | |
| 11:45 | System: *SAT, A Platform for the Development of Modal Decision Procedures |
| Enrico Giunchiglia and Armando Tacchella | |
| 11:55 | System: DLP |
| Peter F. Patel-Schneider | |
| 12:05 | System: Two Techniques to Improve Finite Model Search |
| Audemard Gilles, Benhamou Belaid, Henocque Laurent | |
| 12:15 | Lunch |
| 1:15 | CADE Business Meeting |
| 2:00 | Eliminating Dummy Elimination |
| Jurgen Giesl and Aart Middeldorp | |
| 2:30 | Extending Decision Procedures with Induction Schemes |
| Deepak Kapur and M. Subramaniam | |
| 3:00 | Complete Monotonic Semantic Path Orderings |
| Cristina Borralleras, Maria Ferreira and Albert Rubio | |
| 3:30 | Break |
| 4:00 | Stratified Resolution |
| Anatoli Degtyarev and Andrei Voronkov | |
| 4:30 | Support Ordered Resolution |
| Bruce Spencer and J. D. Horton | |
| 5:00 | System: IVY |
| William McCune and Olga Shumsky | |
| 5:10 | System: SystemOnTPTP |
| Geoff Sutcliffe | |
| 5:20 | System: PTTP+GLiDes, Semantically Guided PTTP |
| Marianne Brown and Geoff Sutcliffe | |
| 5:30 | End of Session |
| 6:00 | CASC Result Presentation |
| Geoff Sutcliffe and Division Winners | |
| 6:30 | CASC Panel Discussion |
| |
|
| Tuesday, June 20 | |
| |
|
| 8:45 | A Formalization of a Concurrent Object Calculus up to Alpha-Conversion |
| Guillaume Gillard | |
| 9:15 | A Resolution Decision Procedure for Fluted Logic |
| Renate A. Schmidt and Ullrich Hustadt | |
| 9:45 | System: ZRes: Meeting of the Old Davis-Putnam procedure with ZBDD |
| Philippe Chatalic and Laurent Simon | |
| 9:55 | System: MBase and Open Mathematical Knowledge Base |
| Andreas Franke and Michael Kohlhase | |
| 10:05 | System: TRAMP: Proof Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level |
| Andreas Meier | |
| 10:15 | Break |
| 10:45 | On Unification for Bounded Distributive Lattices |
| Viorica Sofronie-Stokkermans | |
| 11:15 | Reasoning with Individuals for the Description Logic SHIQ |
| Ian Horrocks, Ulrike Sattler and Stephan Tobies | |
| 11:45 | System: Embedding Verification into Microsoft Excel |
| Graham Collins and Louise A. Dennis | |
| 11:55 | System: Interactive Proof Critics in XBarnacle |
| Helen Lowe and Mike Jackson | |
| 12:05 | End of CADE Technical Program |
| 12:15 | Lunch |
| Afternoon: Workshops and Tutorials | |
| |
|
| Wednesday, June 21, Morning: Workshops | |
| |
|
[ Home
| Program
| Workshops
| Tutorials
| System Competition
]
[ Accommodations
| Excursions
| Computing Facilities
| Athletic Facilities
| Restaurants
| Travel
]
[ On-Line Registration ]
[ UNIF 2000 ]