Program [Printable version]
This program is preliminary and therefore subject to change.
Program at a glance [Goto detailed program]
| Saturday 22 November |
Sunday 23 November |
Monday 24 November |
Tuesday 25 November |
Wednesday 26 November |
Thursday 27 November |
|
|---|---|---|---|---|---|---|
| 9:00 | Workshops | Registration | Invited Speaker | Invited Speaker | Invited Speaker | Session 10 |
| 9:30 | Welcome | |||||
| 10:00 | Break | Break | Excursion | Break | Break | |
| 10:30 | Break | Session 1 | Session 4 | Session 7 | Session 11 | |
| 11:30 | Workshops | |||||
| 12:00 | ||||||
| 12:15 | Short Talks 1 | Short Talks 2 | Short Talks 3 | Short Talks 4 | ||
| 12:45 | Lunch | Lunch | Lunch | Lunch | Lunch | |
| 14:15 | Workshops | Session 2 | Session 5 | Session 8 | Session 12 | |
| 15:00 | ||||||
| 15:40 | Closing | |||||
| 16:00 | Break | Break | Break | Break | Break | |
| 16:30 | Workshops | Session 3 | Session 6 | Session 9 | ||
| 17:00 | ||||||
| 18:15 |
Welcome Reception |
|||||
| 19:30 | Conference dinner | Dinner cruise | ||||
Detailed Technical Program
SATURDAY 22 November 2008
| 8:45 |
CMU-Q
Morning Workshops
Room 1199: ALICS - Applications of Logic in Computer Security (program) Room 1202: IWIL - International Workshop on Implementations of Logic (program) |
| 10:30 |
CMU-Q, outside LH 1202
Break
|
| 11:00 |
CMU-Q
Morning Workshops
Room 1199: ALICS - Applications of Logic in Computer Security (program) Room 1202: IWIL - International Workshop on Implementations of Logic (program) |
| 12:45 |
LAS Cafeteria
Lunch
|
| 14:15 |
CMU-Q
Afternoon Workshops
Room 1199: APS-4 - Analytic Proof Systems 4 (program) Room 1202: KEAPPA - Knowledge Exchange: Automated Provers and Proof Assistants (program) |
| 16:00 |
CMU-Q, outside LH 1202
Break
|
| 16:30 |
CMU-Q
Afternoon Workshops
Room 1199: APS-4 - Analytic Proof Systems 4 (program) Room 1202: KEAPPA - Knowledge Exchange: Automated Provers and Proof Assistants (program) |
| 18:30 |
CMU-Q Atrium
Reception
|
SUNDAY 23 November 2008
| 9:00 |
CMU-Q, Outside Lecture Hall 1202
Registration
|
| 9:30 |
CMU-Q, Lecture Hall 1202
WELCOME
Iliano Cervesato (Carnegie Mellon University, Qatar), General Chair I. Cervesato (CMU, Qatar), H. Veith (TU Darmstadt, Germany), A. Voronkov (U. Manchester, UK), Program Co-Chairs Chuck Thorpe (Carnegie Mellon University, Qatar), Dean |
| 10:00 |
CMU-Q, outside LH 1202
Break
|
| 10:30 |
CMU-Q, Lecture Hall 1202
Constraint Solving
(chaired by N. Bjorner)
Symmetry Breaking for Maximum Satisfiability Joao Marques-Silva (U. Southampton, UK), Ines Lynce (UT Lisboa, Portugal) and Vasco Manquinho (IST/UTL - INESC-ID, Portugal) Efficient Generation of Unsatisfiability Proofs and Cores in SAT Roberto Asín Achá, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez Carbonell (TU Catalonia, Spain) Justification-Based Local Search with Adaptive Noise Strategies Matti Järvisalo, Tommi Junttila and Ilkka Niemelä (Helsinki U. of Technology, Finland) The Max-Atom Problem and its Relevance Marc Bezem (U. Bergen, Norway), Robert Nieuwenhuis and Enric Rodríguez Carbonell (TU Catalonia, Spain) |
| 12:15 |
CMU-Q, Lecture Hall 1202
Short Talks 1
(chaired by R. Pitchler)
Some Remarks on Human Reasoning, Logic Programming and Connectionist Systems Steffen Hölldobler (TU Dresden, Germany) Open Sequential Global Constraints Michael Maher (NICT and U. New South Wales, Australia) Program Development by Proof Transformation: Recent Evolutions Luca Chiarabini (LMU Munich, Germany) |
| 12:45 |
LAS Cafeteria
Lunch
|
| 14:15 |
CMU-Q, Lecture Hall 1202
Knowledge Representation 1
(chaired by M. Maher)
Towards Practical Feasibility of Core Computation in Data Exchange Vadim Savenkov and Reinhard Pichler (TU Vienna, Austria) Data-Oblivious Stream Productivity Joerg Endrullis (Vrije U. Amsterdam, Netherlands), Clemens Grabmayer (U. Utrecht, Netherlands) and Dimitri Hendriks (Vrije U. Amsterdam, Netherlands) Reasoning about XML with Temporal Logics and Automata Leonid Libkin and Cristina Sirangelo (U. Edinburgh, UK) Distributed Consistency-Based Diagnosis Vincent Armant, Philippe Dague and Laurent Simon (LRI - U. Paris Sud, France) |
| 16:00 |
CMU-Q, outside LH 1202
Break
|
| 16:30 |
CMU-Q, Lecture Hall 1202
Proof-Theory 1
(chaired by I. Cervesato)
From one Session to many: Dynamic Tags for Security Protocols Myrto Arapinis, Stéphanie Delaune and Steve Kremer (ENS Cachan, France) A Conditional Logical Framework Furio Honsell, Marina Lenisa (U. Udine, Italy), Luigi Liquori (INRIA- Sophia Antipolis, France) and Ivan Scagnetto (U. Udine, Italy) Nominal renaming sets Murdoch Gabbay (Heriot-Watt U., UK) and Martin Hofmann (LMU Munich, Germany) Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic (tool paper) Sean McLaughlin and Frank Pfenning (Carnegie Mellon U., USA) |
MONDAY 24 November 2008
| 9:00 |
CMU-Q, Lecture Hall 1202
Invited Speaker:
Edmund Clarke
(Carnegie Mellon University, USA)
Chaired by H. Veith Model Checking - My 27-year Quest to Overcome the State Explosion Problem |
| 10:00 |
CMU-Q, outside LH 1202
Break
|
| 10:30 |
CMU-Q, Lecture Hall 1202
Automata
(chaired by A. Bauer)
On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word Automata Benjamin Aminof, Orna Kupferman and Omer Lev (Hebrew U., Israel) Recurrent Reachability Analysis in Regular Model Checking Leonid Libkin and Anthony Widjaja To (U. Edinburgh, UK) Alternation Elimination by Complementation Christian Dax and Felix Klaedtke (ETH Zurich, Switzerland) Discounted Properties of Probabilistic Pushdown Automata Tomas Brazdil, Vaclav Brozek, Jan Holecek and Antonin Kucera (Masaryk U., Czech Republic) |
| 12:15 |
CMU-Q, Lecture Hall 1202
Short Talks 2
(chaired by G. Moser)
Effective CNF Encodings for the Towers of Hanoi Ruben Martins and Ines Lynce (UT Lisbon, Portugal) The Maude-NRL Protocol Analyzer Santiago Escobar (TU Valencia, Spain), Catherine Meadows (NRL, US) and Jose Meseguer (UIUC, US) Requirements for Logical Models for Value-Added Tax Legislation Morten Ib Nielsen, Jakob Grue Simonsen (U. Copenhagen, Denmark) and Ken Friis Larsen (DIKU, Denmark) |
| 12:45 |
LAS Cafeteria
Lunch
|
| 14:15 |
CMU-Q, Lecture Hall 1202
Linear Arithmetic
(chaired by L. de Moura)
A Quantifier Elimination Algorithm for Linear Real Arithmetic David Monniaux (CNRS/VERIMAG, France) ME(LIA) - Model Evolution with Linear Integer Arithmetic Constraints Peter Baumgartner (NICT, Australia), Alexander Fuchs and Cesare Tinelli (U. Iowa, USA) A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic Philipp Ruemmer (Chalmers UT, Sweden) Encoding Queues in Satisfiability Modulo Theories based Bounded Model Checking Tommi Junttila and Jori Dubrovin (Helsinki UT, Finland) |
| 16:00 |
CMU-Q, outside LH 1202
Break
|
| 16:30 |
CMU-Q, Lecture Hall 1202
Verification
(chaired by O. Kupfermann)
On bounded reachability of programs with set comprehensions Margus Veanes (Microsoft Research, USA) and Ando Saabas (Tallinn UT, Estonia) Module Checking of Hierarchical State Machines Aniello Murano (U. Napoli, Italy), Margherita Napoli and Mimmo Parente (U. Salerno, Italy) VALIGATOR: A Verification Tool with Bound and Invariant Generation (tool paper) Thomas Henzinger, Thibaud Hottelier and Laura Kovacs (EPFL, Switzerland) Reveal: A Formal Verification Tool for Verilog (tool paper) Zaher Andraus and Karem Sakallah (U. Michigan, USA) |
| 19:30 |
Assaha Restaurant
Conference dinner
|
TUESDAY 25 November 2008
| 9:00 |
CMU-Q, Lecture Hall 1202
Invited Speaker:
Thomas Eiter
(Technical University of Vienna, Austria)
Chaired by D. Miller Reasoning Using Knots |
| 10:00 |
Sand dunes
Excursion
|
WEDNESDAY 26 November 2008
| 9:00 |
CMU-Q, Lecture Hall 1202
Invited Speaker:
Michael Backes
(Saarland University and MPI-SWS, Germany)
Chaired by I. Cervesato A Formal Language for Cryptographic Pseudocode |
| 10:00 |
CMU-Q, outside LH 1202
Break
|
| 10:30 |
CMU-Q, Lecture Hall 1202
Knowledge Representation 2
(chaired by T. Eiter)
Role Conjunctions in Expressive Description Logics Birte Glimm and Yevgeny Kazakov (U. Oxford, UK) Default Logics with Preference Order: Principles and Characterisations Tore Langholm (U. Oslo, Norway) On Computing Constraint Abduction Answers Michael Maher and Ge Huang (NICT and U. New South Wales, Australia) Fast Counting with Bounded Treewidth Michael Jakl, Reinhard Pichler, Stefan Ruemmele and Stefan Woltran (TU Vienna, Austria) |
| 12:15 |
CMU-Q, Lecture Hall 1202
Short Talks 3
(chaired by M. Samer)
Using Automated Theorem Provers in Nonassociative Algebra David Stanovsky (Charles U., Czech Republic) and J.D. Phillips (Wabash College, US) Accelerating lemma learning using joins - DPLL(Join) Nikolaj Bjorner, Leonardo de Moura (MSR, US) and Bruno Dutertre (SRI, US) Linear algebra techniques for deciding the correctness of probabilistic programs with bounded resources Amilcar Sernadas, Jaime Ramos and Paulo Mateus (IST-TU Lisbon, Portugal) |
| 12:45 |
LAS Cafeteria
Lunch
|
| 14:15 |
CMU-Q, Lecture Hall 1202
Proof-Theory 2
(chaired by M. Hofmann)
Cut elimination for first order Gödel logic by hyperclause resolution Matthias Baaz, Agata Ciabattoni and Christian Fermüller (TU Vienna, Austria) Strategies in the sequent calculus of synthetic connectives Kaustuv Chaudhuri (INRIA Saclay, France) An algorithmic interpretation of a deep inference system Kai Brünnler and Richard McKinley (U. Bern, Switzerland) Weak Normalization and Normalization by Evaluation for System F Andreas Abel (LMU Munich, Germany) |
| 16:00 |
CMU-Q, outside LH 1202
Break
|
| 16:30 |
CMU-Q, Lecture Hall 1202
Quantified Constraints
(chaired by M. Maher)
Variable Dependencies of Quantified CSPs Marko Samer (Durham U., UK) Treewidth: a useful marker of empirical hardness in quantified Boolean logic encodings Luca Pulina and Armando Tacchella (U. Genova, Italy) Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates Witold Charatonik and Michał Wrona (U. Wrocław, Poland) A Logic of Singly Indexed Arrays Radu Iosif (U. Grenoble, France), Peter Habermehl (U. Paris 7, France) and Tomas Vojnar (Brno UT, Czech Republic) |
| 19:30 |
Doha Bay
Dinner cruise
|
THURSDAY 27 November 2008
| 9:00 |
CMU-Q, Lecture Hall 1202
Rewriting 1
(chaired by A. Middeldorp)
Improving Context-Sensitive Dependency Pairs Beatriz Alarcón (UP Valencia, Spain), Fabian Emmes, Carsten Fuhs, Jürgen Giesl (RWTH Aachen, Germany), Raúl Gutierrez, Salvador Lucas (UP Valencia, Spain), Peter Schneider-Kamp (RWTH Aachen, Germany) and Renè Thiemann (U. Innsbruck, Austria) Complexity, Graphs, and the Dependency Pair Method Nao Hirokawa (JAIST, Japan) and Georg Moser (U. Innsbruck, Austria) |
| 10:00 |
CMU-Q, outside LH 1202
Break
|
| 10:30 |
CMU-Q, Lecture Hall 1202
Modal and Temporal Logics
(chaired by D. Monniaux)
On the computational complexity of spatial logics with connectedness constraints Roman Kontchakov (Birkbeck College, UK), Ian Pratt-Hartmann (U. Manchester, UK), Frank Wolter (U. Liverpool, UK) and Michael Zakharyaschev (Birkbeck College, UK) Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification Davide Bresolin (U. Verona, Italy), Dario Della Monica (U. Udine, Italy), Valentin Goranko (U. Witswatersrand, South Africa), Angelo Montanari (U. Udine, Italy) and Guido Sciavicco (U. Murcia, Spain) The Variable Hierarchy for the Games mu-Calculus Walid Belkhir and Luigi Santocanale (U. Provence, France) A Formalised Lower Bound on Undirected Graph Reachability Ulrich Schoepp (LMU Munich, Germany) |
| 12:15 |
CMU-Q, Lecture Hall 1202
Short Talks 4
(chaired by L. Liquori)
Temporal Reasoning for Machine Code Nadeem Hamid (Berry College, US) |
| 12:45 |
LAS Cafeteria
Lunch
|
| 14:15 |
CMU-Q, Lecture Hall 1202
Rewriting 2
(chaired by G. Moser)
Uncurrying for Termination Nao Hirokawa (JAIST, Japan), Aart Middeldorp and Harald Zankl (U. Innsbruck, Austria) Approximating Term Rewriting Systems: a Horn Clause Specification and its Implementation John Gallagher and Mads Rosendahl (Roskilde U., Denmark) A higher-order iterative path ordering Cynthia Kop and Femke van Raamsdonk (Vrije U. Amsterdam, Netherlands) |
| 15:40 |
CMU-Q, Lecture Hall 1202
Closing Remarks
Iliano Cervesato (Carnegie Mellon University, Qatar), Helmut Veith (Technical University of Darmstadt, Germany), Andrei Voronkov (University of Manchester, UK), Program Co-Chairs |
| 16:00 |
CMU-Q, outside LH 1202
Break
|
Sponsorship
For information on exhibition and sponsorship opportunities at the conference, contact Iliano Cervesato at
Press and Media
For media-related inquiries, contact Noha Al Afifi at
Please send email to for any additional information.