15. LPAR 2008: Doha, Qatar

Constraint Solving

• João Marques-Silva, Inês Lynce, Vasco M. Manquinho:
  Symmetry Breaking for Maximum Satisfiability. 1-15
  Electronic Edition (link) BibTeX
• Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
  Efficient Generation of Unsatisfiability Proofs and Cores in SAT. 16-30
  Electronic Edition (link) BibTeX
• Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä:
  Justification-Based Local Search with Adaptive Noise Strategies. 31-46
  Electronic Edition (link) BibTeX
• Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell:
  The Max-Atom Problem and Its Relevance. 47-61
  Electronic Edition (link) BibTeX

Knowledge Representation 1

• Reinhard Pichler, Vadim Savenkov:
  Towards Practical Feasibility of Core Computation in Data Exchange. 62-78
  Electronic Edition (link) BibTeX
• Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks:
  Data-Oblivious Stream Productivity. 79-96
  Electronic Edition (link) BibTeX
• Leonid Libkin, Cristina Sirangelo:
  Reasoning about XML with Temporal Logics and Automata. 97-112
  Electronic Edition (link) BibTeX
• Vincent Armant, Philippe Dague, Laurent Simon:
  Distributed Consistency-Based Diagnosis. 113-127
  Electronic Edition (link) BibTeX

Proof-Theory 1

• Myrto Arapinis, Stéphanie Delaune, Steve Kremer:
  From One Session to Many: Dynamic Tags for Security Protocols. 128-142
  Electronic Edition (link) BibTeX
• Furio Honsell, Marina Lenisa, Luigi Liquori, Ivan Scagnetto:
  A Conditional Logical Framework. 143-157
  Electronic Edition (link) BibTeX
• Murdoch James Gabbay, Martin Hofmann:
  Nominal Renaming Sets. 158-173
  Electronic Edition (link) BibTeX
• Sean McLaughlin, Frank Pfenning:
  Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. 174-181
  Electronic Edition (link) BibTeX

Invited Talk

• Edmund M. Clarke:
  Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. 182
  Electronic Edition (link) BibTeX

Automata

• Benjamin Aminof, Orna Kupferman, Omer Lev:
  On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word Automata. 183-197
  Electronic Edition (link) BibTeX
• Anthony Widjaja To, Leonid Libkin:
  Recurrent Reachability Analysis in Regular Model Checking. 198-213
  Electronic Edition (link) BibTeX
• Christian Dax, Felix Klaedtke:
  Alternation Elimination by Complementation (Extended Abstract). 214-229
  Electronic Edition (link) BibTeX
• Tomás Brázdil, Václav Brozek, Jan Holecek, Antonín Kucera:
  Discounted Properties of Probabilistic Pushdown Automata. 230-242
  Electronic Edition (link) BibTeX

Linear Arithmetic

• David Monniaux:
  A Quantifier Elimination Algorithm for Linear Real Arithmetic. 243-257
  Electronic Edition (link) BibTeX
• Peter Baumgartner, Alexander Fuchs, Cesare Tinelli:
  (LIA) - Model Evolution with Linear Integer Arithmetic Constraints. 258-273
  Electronic Edition (link) BibTeX
• Philipp Rümmer:
  A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. 274-289
  Electronic Edition (link) BibTeX
• Tommi A. Junttila, Jori Dubrovin:
  Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking. 290-304
  Electronic Edition (link) BibTeX

Verification

• Margus Veanes, Ando Saabas:
  On Bounded Reachability of Programs with Set Comprehensions. 305-317
  Electronic Edition (link) BibTeX
• Aniello Murano, Margherita Napoli, Mimmo Parente:
  Program Complexity in Hierarchical Module Checking. 318-332
  Electronic Edition (link) BibTeX
• Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács:
  Valigator: A Verification Tool with Bound and Invariant Generation. 333-342
  Electronic Edition (link) BibTeX
• Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah:
  Reveal: A Formal Verification Tool for Verilog Designs. 343-352
  Electronic Edition (link) BibTeX

Invited Talks

• Michael Backes, Matthias Berg, Dominique Unruh:
  A Formal Language for Cryptographic Pseudocode. 353-376
  Electronic Edition (link) BibTeX
• Thomas Eiter, Magdalena Ortiz, Mantas Simkus:
  Reasoning Using Knots. 377-390
  Electronic Edition (link) BibTeX

Knowledge Representation 2

• Birte Glimm, Yevgeny Kazakov:
  Role Conjunctions in Expressive Description Logics. 391-405
  Electronic Edition (link) BibTeX
• Tore Langholm:
  Default Logics with Preference Order: Principles and Characterisations. 406-420
  Electronic Edition (link) BibTeX
• Michael J. Maher, Ge Huang:
  On Computing Constraint Abduction Answers. 421-435
  Electronic Edition (link) BibTeX
• Michael Jakl, Reinhard Pichler, Stefan Rümmele, Stefan Woltran:
  Fast Counting with Bounded Treewidth. 436-450
  Electronic Edition (link) BibTeX

Proof-Theory 2

• Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller:
  Cut Elimination for First Order Gödel Logic by Hyperclause Resolution. 451-466
  Electronic Edition (link) BibTeX
• Kaustuv Chaudhuri:
  Focusing Strategies in the Sequent Calculus of Synthetic Connectives. 467-481
  Electronic Edition (link) BibTeX
• Kai Brünnler, Richard McKinley:
  An Algorithmic Interpretation of a Deep Inference System. 482-496
  Electronic Edition (link) BibTeX
• Andreas Abel:
  Weak beta-theta-Normalization and Normalization by Evaluation for System F. 497-511
  Electronic Edition (link) BibTeX

Quantified Constraints

• Marko Samer:
  Variable Dependencies of Quantified CSPs. 512-527
  Electronic Edition (link) BibTeX
• Luca Pulina, Armando Tacchella:
  Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings. 528-542
  Electronic Edition (link) BibTeX
• Witold Charatonik, Michal Wrona:
  Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates. 543-557
  Electronic Edition (link) BibTeX
• Peter Habermehl, Radu Iosif, Tomás Vojnar:
  A Logic of Singly Indexed Arrays. 558-573
  Electronic Edition (link) BibTeX

Modal and Temporal Logics

• Roman Kontchakov, Ian Pratt-Hartmann, Frank Wolter, Michael Zakharyaschev:
  On the Computational Complexity of Spatial Logics with Connectedness Constraints. 574-589
  Electronic Edition (link) BibTeX
• Davide Bresolin, Dario Della Monica, Valentin Goranko, Angelo Montanari, Guido Sciavicco:
  Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification. 590-604
  Electronic Edition (link) BibTeX
• Walid Belkhir, Luigi Santocanale:
  The Variable Hierarchy for the Lattice µ-Calculus. 605-620
  Electronic Edition (link) BibTeX
• Ulrich Schöpp:
  A Formalised Lower Bound on Undirected Graph Reachability. 621-635
  Electronic Edition (link) BibTeX

Rewriting

• Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann:
  Improving Context-Sensitive Dependency Pairs. 636-651
  Electronic Edition (link) BibTeX
• Nao Hirokawa, Georg Moser:
  Complexity, Graphs, and the Dependency Pair Method. 652-666
  Electronic Edition (link) BibTeX
• Nao Hirokawa, Aart Middeldorp, Harald Zankl:
  Uncurrying for Termination. 667-681
  Electronic Edition (link) BibTeX
• John P. Gallagher, Mads Rosendahl:
  Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation. 682-696
  Electronic Edition (link) BibTeX
• Cynthia Kop, Femke van Raamsdonk:
  A Higher-Order Iterative Path Ordering. 697-711
  Electronic Edition (link) BibTeX