![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
Sessions take place in auditorium 3 unless otherwise indicated.
Saturday July 27th
Saturday's program is also available with abstracts or side by side with other meetings.09:00-10:30 Session 1: Description logics and Semantic Web
| 09:00 | Ian Horrocks, U Manchester,
UK Invited talk: Reasoning with expressive description logics: Theory and practice |
| 10:00 | Guoqiang
Pan, Rice U, USA; Ulrike Sattler, Dresden U of Techn., Germany; and Moshe Y.
Vardi, Rice U, USA BDD-based decision procedures for K |
10:30-11:00 Refreshments
11:00-12:30 Session 2: Proof-carrying code and compiler verification
| 11:00 | Andrew
Bernard and Peter Lee, Carnegie Mellon U, USA Temporal logic for proof-carrying code |
| 11:30 | George
C. Necula and Robert R. Schneck, U California-Berkeley, USA A gradual approach to a more trustworthy, yet scalable, proof-carrying code |
| 12:00 | Martin
Strecker, Techn. U of Munich, Germany Formal verification of a java compiler in isabelle |
12:30-14:00 Lunch
14:00-15:30 Session 3: Non-classical logics
| 14:00 | Uwe
Egly, Vienna U of Techn., Austria Embedding lax logic into intuitionistic logic |
| 14:30 | Dominique
Larchey-Wendling, LORIA Nancy, France Combining proof-search and counter-model construction for deciding Gödel-Dummett logic |
| 15:00 | Didier
Galmiche and Daniel Mery, LORIA Nancy, France Connection-based proof search in propositional BI logic |
15:30-16:00 Refreshments
16:00-17:30 Session 4: System descriptions
| 16:00 | Jesper
Møller, IT U of Copenhagen, Denmark System description: DDDLIB: A library for solving quantified difference inequalities |
| 16:15 | Joe
Hurd, U Cambridge, UK System description: An LCF-style interface between HOL and first-order logic |
| 16:30 | Michael
Kohlhase, Carnegie Mellon U, USA and Jürgen Zimmer, Saarland U, Germany System description: System description: The MathWeb software bus for distributed mathmatical reasoning |
| 16:45 | Jörg
Siekmann, Saarland U, Germany et al. System description: Proof development with OMEGA |
| 17:00 | Mateja
Jamnik, U Cambridge, UK; Manfred Kerber, U Birmingham, UK; and Martin Pollet,
Saarland U, Germany System description: LearnOmatic: System description |
| 17:15 | Carlos
E. Areces and Juan Heguiabehere, U Amsterdam, The Netherlands System description: HyLoRes 1.0: Direct resolution for hybrid logics |
17:30-19:00 Welcome reception (joint
with CAV)
Room:
Lobby
19:30-21:00 CASC dinner
Room:
Restaurant Da Mario
Sunday July 28th
Sunday's program is also available with abstracts or side by side with other meetings.- 08:30-16:00 in Aud. 4: Live competition updates
09:00-10:30 Session 5: SAT
| 09:00 | Eugene
Goldberg, Cadence Design Systems, USA Testing satisfiability of CNF formulas by computing a stable set of points |
| 09:30 | Thierry
Boy de la Tour, IMAG Grenoble, France A note on symmetry heuristics in SEM |
| 10:00 | Gilles
Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, and
Roberto Sebastiani; ITC-irst, Italy A SAT based approach for solving formulas over boolean and linear mathematical propositions |
10:30-11:00 Refreshments
11:00-12:30 Session 6: Model generation
| 11:00 | Wolfgang
Ahrendt, Chalmers U of Techn., Sweden Deductive search for errors in free data type specifications using model generation |
| 11:30 | Gilles
Audemard, ITC-irst, Italy and Belaid Benhamou, LSIS Marseille, France Reasoning by symmetry and function ordering in finite model generation |
| 12:00 | Bernhard
Gramlich and Reinhard Pichler, Vienna U of Techn., Austria Algorithmic aspects of herbrand models represented by ground atoms with ground equations |
12:30-14:00 Lunch
14:00-15:30 Session 7
| 14:00 | Daniel Jackson, Massachusetts Inst. of
Techn., USA Invited talk: Simple logic, complex systems |
| 15:00 | Lilia
Georgieva, U Manchester, UK; Ullrich Hustadt, U Liverpool, UK; and Renate A.
Schmidt, U Manchester, UK A new clausal class decidable by hyperresolution |
15:30-16:00 Refreshments
16:00-17:00 Session 8: CASC
| 16:00 | Christoph
Weidenbach, Opel AG, Germany; Uwe Brahm, MPI Saarbrücken, Germany; Thomas
Hillenbrand, MPI Saarbrücken, Germany; Enno Keen, MPI Saarbrücken, Germany;
Christian Theobalt, MPI Saarbrücken, Germany; and Dalibor Topic, MPI
Saarbrücken, Germany System description: SPASS version 2.0 |
| 16:15 | Stephan
Schulz, Techn. U of Munich, Germany and Geoff Sutcliffe, U Miami, USA System description: System description: GrAnDe 1.0 |
| 16:30 | Simon
Colton, U Edinburgh, UK System description: System description: The HR program for theorem generation |
| 16:45 | Michael
Whalen, U Minnesota, USA; Johann Schumann, NASA Ames, USA; and Bernd Fischer,
NASA Ames, USA System description: AutoBayes/CC - combining program synthesis with automatic code certification - system description |
17:00-18:00 Herbrand award
| 17:00 | Award ceremony |
| 17:10 | Mark Stickel, SRI International, USA (Acceptance speech) |
18:00-18:30 CASC (continued)
| 18:00 | CASC results and discussion |
19:30-22:00 Conference dinner
Room:
Restaurant Luftkastellet
Monday July 29th
Monday's program is also available with abstracts or side by side with other meetings.09:00-10:00 Invited talk (joint with
CAV)
Room:
auditorium 1
| 09:00 | Sharad Malik, Princeton U,
USA Invited talk: The quest for efficient Boolean satisfiability solvers |
10:00-10:30 Session 9
| 10:00 | Cristina
Borralleras, U Vic, Spain; Salvador Lucas, Polytechnic U of Valencia, Spain;
and Albert Rubio, Techn. U of Catalonia, Spain Recursive path orderings can be context-sensitive |
10:30-11:00 Refreshments
11:00-12:30 Session 10: Combination of Decision Procedures
| 11:00 | Harald
Ganzinger, MPI Saarbrücken, Germany Shostak light |
| 11:30 | Jonathan
Ford, U New England, Australia and Natarajan Shankar, SRI International,
USA Formal verification of a combination decision procedure |
| 12:00 | Calogero
G. Zarba, Stanford U, USA Combining multisets with integers |
12:30-14:00 Lunch
14:00-15:30 Session 11: Logical frameworks
| 14:00 | Lawrence
C. Paulson, U Cambridge, UK The reflection theorem: A study in formalizing meta-theoretic reasoning |
| 14:30 | Aaron
Stump and David L. Dill, Stanford U, USA Faster proof checking in the Edinburgh Logical Framework |
| 15:00 | Chad
E. Brown, Carnegie Mellon U, USA Solving for set variables in higher-order theorem proving |
15:30-16:00 Refreshments
16:00-17:00 Session 12: Model checking
| 16:00 | Orna
Kupferman, Hebrew U of Jerusalem, Israel; Ulrike Sattler, Dresden U of Techn.,
Germany; and Moshe Y. Vardi, Rice U, USA The complexity of the graded µ-calculus |
| 16:30 | Leonardo
de Moura, Harald Rueß, and Maria Sorea; SRI International, USA Lazy theorem proving for bounded model checking over infinite domains |
17:00-18:00 CADE business meeting
19:00-21:00 City Hall reception
(joint with CAV, ICLP, TABLEAUX)
Room:
City Hall
Tuesday July 30th
Tuesday's program is also available with abstracts or side by side with other meetings.09:00-10:30 Session 13: Equational reasoning
| 09:00 | Miquel
Bofill, U Girona, Spain and Albert Rubio, Techn. U of Catalonia, Spain Well-foundedness is sufficient for completeness of ordered paramodulation |
| 09:30 | Christopher
Lynch and Barbara Morawska, Clarkson U, USA Basic syntactic mutation |
| 10:00 | Thomas
Hillenbrand, MPI Saarbrücken, Germany and Bernd Löchner, U Kaiserslautern,
Germany The next Waldmeister loop |
10:30-11:00 Refreshments
11:00-11:30 Session 14: Proof theory
| 11:00 | Jean-Marc
Andreoli, Xerox Grenoble, France Focussing proof-net construction as a middleware paradigm |
11:30-12:30 Invited talk (joint with TABLEAUX)
| 11:30 | Matthias Baaz, Vienna U of Techn.,
Austria Invited talk: Proof analysis by resolution |
12:30-14:00 Lunch
| FLoC |
|
| MEETINGS |
|
| PROGRAM |
|
| FACILITIES |
|
| COPENHAGEN |
|
| MISCELLANEOUS |
|
