Constraint Solving

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

Knowledge Representation 1

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

Proof-Theory 1

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

Invited Talk

• 
  Edmund M. Clarke: Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. 182

Automata

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

Linear Arithmetic

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

Verification

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

Invited Talks

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

Knowledge Representation 2

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

Proof-Theory 2

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

Quantified Constraints

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

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
• 
  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
• 
  Walid Belkhir, Luigi Santocanale: The Variable Hierarchy for the Lattice µ-Calculus. 605-620
• 
  Ulrich Schöpp: A Formalised Lower Bound on Undirected Graph Reachability. 621-635

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
• 
  Nao Hirokawa, Georg Moser: Complexity, Graphs, and the Dependency Pair Method. 652-666
• 
  Nao Hirokawa, Aart Middeldorp, Harald Zankl: Uncurrying for Termination. 667-681
• 
  John P. Gallagher, Mads Rosendahl: Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation. 682-696
• 
  Cynthia Kop, Femke van Raamsdonk: A Higher-Order Iterative Path Ordering. 697-711

last updated on Sat May 25 05:21:30 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page