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 |
|