LPAR 2008

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	Invited Speaker	Invited Speaker	Invited Speaker	Session 10
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						Session 12
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	Welcome Reception		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