CADE program

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.

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