Abstract is missing.
- Symmetry Breaking for Maximum SatisfiabilityJoão Marques-Silva, Inês Lynce, Vasco M. Manquinho. 1-15 [doi]
- Efficient Generation of Unsatisfiability Proofs and Cores in SATRoberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. 16-30 [doi]
- Justification-Based Local Search with Adaptive Noise StrategiesMatti Järvisalo, Tommi A. Junttila, Ilkka Niemelä. 31-46 [doi]
- The Max-Atom Problem and Its RelevanceMarc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell. 47-61 [doi]
- Towards Practical Feasibility of Core Computation in Data ExchangeReinhard Pichler, Vadim Savenkov. 62-78 [doi]
- Data-Oblivious Stream ProductivityJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks. 79-96 [doi]
- Reasoning about XML with Temporal Logics and AutomataLeonid Libkin, Cristina Sirangelo. 97-112 [doi]
- Distributed Consistency-Based DiagnosisVincent Armant, Philippe Dague, Laurent Simon. 113-127 [doi]
- From One Session to Many: Dynamic Tags for Security ProtocolsMyrto Arapinis, Stéphanie Delaune, Steve Kremer. 128-142 [doi]
- A Conditional Logical FrameworkFurio Honsell, Marina Lenisa, Luigi Liquori, Ivan Scagnetto. 143-157 [doi]
- Nominal Renaming SetsMurdoch James Gabbay, Martin Hofmann. 158-173 [doi]
- Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional LogicSean McLaughlin, Frank Pfenning. 174-181 [doi]
- Model Checking - My 27-Year Quest to Overcome the State Explosion ProblemEdmund M. Clarke. 182 [doi]
- On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word AutomataBenjamin Aminof, Orna Kupferman, Omer Lev. 183-197 [doi]
- Recurrent Reachability Analysis in Regular Model CheckingAnthony Widjaja To, Leonid Libkin. 198-213 [doi]
- Alternation Elimination by Complementation (Extended Abstract)Christian Dax, Felix Klaedtke. 214-229 [doi]
- Discounted Properties of Probabilistic Pushdown AutomataTomás Brázdil, Václav Brozek, Jan Holecek, Antonín Kucera. 230-242 [doi]
- A Quantifier Elimination Algorithm for Linear Real ArithmeticDavid Monniaux. 243-257 [doi]
- (LIA) - Model Evolution with Linear Integer Arithmetic ConstraintsPeter Baumgartner, Alexander Fuchs, Cesare Tinelli. 258-273 [doi]
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer ArithmeticPhilipp Rümmer. 274-289 [doi]
- Encoding Queues in Satisfiability Modulo Theories Based Bounded Model CheckingTommi A. Junttila, Jori Dubrovin. 290-304 [doi]
- On Bounded Reachability of Programs with Set ComprehensionsMargus Veanes, Ando Saabas. 305-317 [doi]
- Program Complexity in Hierarchical Module CheckingAniello Murano, Margherita Napoli, Mimmo Parente. 318-332 [doi]
- Valigator: A Verification Tool with Bound and Invariant GenerationThomas A. Henzinger, Thibaud Hottelier, Laura Kovács. 333-342 [doi]
- Reveal: A Formal Verification Tool for Verilog DesignsZaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah. 343-352 [doi]
- A Formal Language for Cryptographic PseudocodeMichael Backes, Matthias Berg, Dominique Unruh. 353-376 [doi]
- Reasoning Using KnotsThomas Eiter, Magdalena Ortiz, Mantas Simkus. 377-390 [doi]
- Role Conjunctions in Expressive Description LogicsBirte Glimm, Yevgeny Kazakov. 391-405 [doi]
- Default Logics with Preference Order: Principles and CharacterisationsTore Langholm. 406-420 [doi]
- On Computing Constraint Abduction AnswersMichael J. Maher, Ge Huang. 421-435 [doi]
- Fast Counting with Bounded TreewidthMichael Jakl, Reinhard Pichler, Stefan Rümmele, Stefan Woltran. 436-450 [doi]
- Cut Elimination for First Order Gödel Logic by Hyperclause ResolutionMatthias Baaz, Agata Ciabattoni, Christian G. Fermüller. 451-466 [doi]
- Focusing Strategies in the Sequent Calculus of Synthetic ConnectivesKaustuv Chaudhuri. 467-481 [doi]
- An Algorithmic Interpretation of a Deep Inference SystemKai Brünnler, Richard McKinley. 482-496 [doi]
- Weak beta-theta-Normalization and Normalization by Evaluation for System FAndreas Abel. 497-511 [doi]
- Variable Dependencies of Quantified CSPsMarko Samer. 512-527 [doi]
- Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic EncodingsLuca Pulina, Armando Tacchella. 528-542 [doi]
- Tractable Quantified Constraint Satisfaction Problems over Positive Temporal TemplatesWitold Charatonik, Michal Wrona. 543-557 [doi]
- A Logic of Singly Indexed ArraysPeter Habermehl, Radu Iosif, Tomás Vojnar. 558-573 [doi]
- On the Computational Complexity of Spatial Logics with Connectedness ConstraintsRoman Kontchakov, Ian Pratt-Hartmann, Frank Wolter, Michael Zakharyaschev. 574-589 [doi]
- Decidable and Undecidable Fragments of Halpern and Shoham s Interval Temporal Logic: Towards a Complete ClassificationDavide Bresolin, Dario Della Monica, Valentin Goranko, Angelo Montanari, Guido Sciavicco. 590-604 [doi]
- The Variable Hierarchy for the Lattice µ-CalculusWalid Belkhir, Luigi Santocanale. 605-620 [doi]
- A Formalised Lower Bound on Undirected Graph ReachabilityUlrich Schöpp. 621-635 [doi]
- Improving Context-Sensitive Dependency PairsBeatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann. 636-651 [doi]
- Complexity, Graphs, and the Dependency Pair MethodNao Hirokawa, Georg Moser. 652-666 [doi]
- Uncurrying for TerminationNao Hirokawa, Aart Middeldorp, Harald Zankl. 667-681 [doi]
- Approximating Term Rewriting Systems: A Horn Clause Specification and Its ImplementationJohn P. Gallagher, Mads Rosendahl. 682-696 [doi]
- A Higher-Order Iterative Path OrderingCynthia Kop, Femke van Raamsdonk. 697-711 [doi]