Volume 174, Number 1, April 2007

Proceedings of the 7th International Workshop on Rule Based Programming (RULE 2006)

• 
  Maribel Fernández, Ralf Lämmel: Preface. 1-2
• 
  José Miguel Cleva, Francisco Javier López-Fraguas: Semantic Determinism and Functional Logic Program Properties. 3-15
• 
  Alcino Cunha, Joost Visser: Strongly Typed Rewriting For Coupled Software Transformation. 17-34
• 
  Florent Kirchner, François-Régis Sinot: Rule-Based Operational Semantics for an Imperative Language. 35-47
• 
  Emanuel Kitzelmann, Ute Schmid: Inducing Constructor Systems from Example-Terms by Detecting Syntactical Regularities. 49-63
• 
  Peter Csaba Ölveczky, José Meseguer: Recent Advances in Real-Time Maude. 65-81
• 
  Fernando Rosa-Velardo: Coding Mobile Synchronizing Petri Nets into Rewriting Logic. 83-98
• 
  Victor L. Winter: Model-driven Transformation-based Generation of Java Stress Tests. 99-114

Volume 174, Number 2, May 2007

Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)

• 
  Serge Autexier, Christoph Benzmüller: Preface. 1-2
• 
  Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J. Strother Moore: ACL2s: "The ACL2 Sedan". 3-18
• 
  Louise A. Dennis: Enhancing Theorem Prover Interfaces with Program Slice Information. 19-33
• 
  Pedro Quaresma, Predrag Janicic: GeoThms - a Web System for Euclidean Constructive Geometry. 35-48
• 
  Cezary Kaliszyk: Web Interfaces for Proof Assistants. 49-61
• 
  Josef Urban, Grzegorz Bancerek: Presenting and Explaining Mizar. 63-74
• 
  Anne Mulhern, Charles Fischer, Ben Liblit: Tool Support for Proof Engineering. 75-86
• 
  Marc Wagner, Serge Autexier, Christoph Benzmüller: PlatOmega: A Mediator between Text-Editors and Proof Assistance Systems. 87-107
• 
  Steven Trac, Yury Puzis, Geoff Sutcliffe: An Interactive Derivation Viewer. 109-123
• 
  Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli: Tinycals: Step by Step Tacticals. 125-142

Volume 174, Number 3, May 2007

Proceedings of the Fourth International Workshop on Bounded Model Checking (BMC 2006)

• 
  Ofer Strichman, Armin Biere: Preface. 1-2
• 
  Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen: Bounded Model Checking with Parametric Data Structures. 3-16
• 
  Paul B. Jackson, Daniel Sheridan: A Compact Linear Translation for Bounded Model Checking. 17-30
• 
  João Marques-Silva: Interpolant Learning and Reuse in SAT-Based Model Checking. 31-43
• 
  Toni Jussila, Armin Biere: Compressing BMC Encodings with QBF. 45-56
• 
  Xuandong Li, Sumit Jha Aanand, Lei Bu: Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming. 57-70

Volume 174, Number 4, May 2007

Proceedings of the Workshop on Verification and Debugging (V&D 2006)

• 
  Roderick Bloem, Marco Roveri, Fabio Somenzi: Preface. 1
• 
  John Moondanos: From Error to Error: Logic Debugging in the Many-Core Era. 3-7
• 
  Alper Sen: Error Diagnosis in Equivalence Checking of High Performance Microprocessors. 9-18
• 
  Lionel van den Berg, Paul A. Strooper, Wendy Johnston: An Automated Approach for the Interpretation of Counter-Examples. 19-35
• 
  Jooyong Lee: Dynamic Reverse Code Generation for Backward Execution. 37-54
• 
  Andreas Zeller: Where Do Bugs Come From? 55-59
• 
  Wolfgang Mayer, Markus Stumptner: Model-Based Debugging - State of the Art And Future Challenges. 61-82
• 
  Irith Pomeranz, Sudhakar M. Reddy: On the Use of Functional Test Generation in Diagnostic Test Generation for Synchronous Sequential Circuits. 83-93
• 
  Andreas Griesmayer, Stefan Staber, Roderick Bloem: Automated Fault Localization for C Programs. 95-111
• 
  Martin C. Rinard: Automated Techniques for Surviving (Otherwise) Fatal Software Errors. 113-116
• 
  Juan Carlos López Pimentel, Raul Monroy, Dieter Hutter: A Method for Patching Interleaving-Replay Attacks in Faulty Security Protocols. 117-130

Volume 174, Number 5, June 2007

Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006)

• 
  Alberto Momigliano, Brigitte Pientka: Preface. 1-2
• 
  Ulrich Schöpp: Modelling Generic Judgements. 19-35
• 
  Murdoch Gabbay: Hierarchical Nominal Terms and Their Theory of Rewriting. 37-52
• 
  Stefan Berghofer, Christian Urban: A Head-to-Head Comparison of de Bruijn Indices and Names. 53-67
• 
  Jason Hickey, Aleksey Nogin, Xin Yu, Alexei Kopylov: Practical Reflection for Sequent Logics. 79-94
• 
  Chad E. Brown: Encoding Functional Relations in Scunak. 127-139
• 
  Alwen Tiu: A Logic for Reasoning about Generic Judgments. 3-18
• 
  Brian E. Aydemir, Aaron Bohannon, Stephanie Weirich: Nominal Reasoning Techniques in Coq: (Extended Abstract). 69-77
• 
  Andrew W. Appel, Xavier Leroy: A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). 95-108
• 
  Kevin Donnelly, Hongwei Xi: A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. 109-125
• 
  Mircea-Dan Hernest: Synthesis of Moduli of Uniform Continuity by the Monotone Dialectica Interpretation in the Proof-system MinLog. 141-149

Volume 174, Number 6, June 2007

Proceedings of the International Workshop on Hybrid Logic (HyLo 2006)

• 
  Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva, Jørgen Villadsen: Preface. 1-2
• 
  Ian Horrocks, Birte Glimm, Ulrike Sattler: Hybrid Logics and Ontology Languages. 3-14
• 
  Moritz Hardt, Gert Smolka: Higher-Order Syntax and Saturation Algorithms for Hybrid Logic. 15-27
• 
  Martin Mundhenk, Thomas Schneider: Undecidability of Multi-modal Hybrid Logics. 29-43
• 
  Nicole Bidoit, Dario Colazzo: Testing XML constraint satisfiability. 45-61
• 
  André Platzer: Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems. 63-77
• 
  Balder ten Cate, Tadeusz Litak: Topological Perspective on the Hybrid Proof Rules. 79-94
• 
  Katsuhiko Sano: A Hybridization of Irreflexive Modal Logics. 95-111
• 
  Thomas Bolander, Jens Ulrik Hansen, Michael R. Hansen: Decidability of a Hybrid Duration Calculus. 113-133
• 
  Jason Reed: Hybridizing a Logical Framework. 135-148

Volume 174, Number 7, June 2007

Proceedings of the Programming Languages meets Program Verification (PLPV 2006)

• 
  Aaron Stump, Hongwei Xi: Preface. 1-2
• 
  James Caldwell, Josef Pohl: Constructive Membership Predicates as Index Types. 3-16
• 
  Adam Chlipala: Position Paper: Thoughts on Programming with Proof Assistants. 17-21
• 
  Louis-Julien Guillemette, Stefan Monnier: Type-Safe Code Transformations in Haskell. 23-39
• 
  Brigitte Pientka: Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions. 41-60
• 
  Andreas Schlosser, Christoph Walther, Michael Gonder, Markus Aderhold: Context Dependent Procedures and Computed Types in -eriFun. 61-78
• 
  Oleg Kiselyov, Chung-chieh Shan: Lightweight Static Capabilities. 79-104
• 
  Tim Sheard: Type-level Computation Using Narrowing in Omegamega. 105-128
• 
  Martin Sulzmann, Razvan Voicu: Language-Based Program Verification via Expressive Types. 129-147

Volume 174, Number 8, June 2007

Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006)

• 
  Michael W. Mislove: Editor's Note. 1
• 
  Byron Cook, Roberto Sebastiani: Preface and Foreword. 3-6
• 
  Sava Krstic, Robert B. Jones, John O'Leary: Mothers of Pipelines. 7-22
• 
  Clark Barrett, Igor Shikanian, Cesare Tinelli: An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. 23-37
• 
  Swen Jacobs, Viorica Sofronie-Stokkermans: Applications of Hierarchical Reasoning in the Verification of Complex Systems. 39-54
• 
  Maria Paola Bonacina, Mnacho Echenim: Rewrite-Based Satisfiability Procedures for Recursive Data Structures. 55-70
• 
  Sayan Mitra, Nancy A. Lynch: Proving Approximate Implementations for Probabilistic I/O Automata. 71-93
• 
  Alessandro Tiberi: Probabilistic Configuration Theories. 95-108

Volume 174, Number 9, June 2007

Proceedings of the Thread Verification Workshop (TV 2006)

• 
  Ganesh Gopalakrishnan, John O'Leary: Preface. 1-4
• 
  Arndt Mühlenfeld, Franz Wotawa: Fault Detection in Multi-Threaded C++ Server Applications. 5-22
• 
  Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte: A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs. 23-47
• 
  Robert P. Cook: Thread Verification - An Experience Report. 49-61
• 
  Lisa Higham, LillAnne Jackson, Jalal Kawash: What is Itanium Memory Consistency from the Programmer's Point of View? 63-84
• 
  Lukasz Ziarek, Philip Schatz, Suresh Jagannathan: Modular Checkpointing for Atomicity. 85-115
• 
  Jan-Willem Maessen, Arvind: Store Atomicity for Transactional Memory. 117-137
• 
  John Regehr, Nathan Cooprider: Interrupt Verification via Thread Verification. 139-150
• 
  Shady Copty, Shmuel Ur: Toward Automatic Concurrent Debugging Via Minimal Program Mutant Generation with AspectJ. 151-165

Volume 174, Number 10, July 2007

Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2006)

• 
  Sergio Antoy: Preface. 1-2
• 
  Richard B. Kieburtz: Programmed Strategies for Program Verification. 3-38
• 
  Horatiu Cirstea, Germain Faure, Maribel Fernández, Ian Mackie, François-Régis Sinot: From Functional Programs to Interaction Nets via the Rewriting Calculus. 39-56
• 
  Sandra Alves, Maribel Fernández, Mário Florido, Ian Mackie: The Power of Closed Reduction Strategies. 57-74
• 
  Naoki Nishida, Tomohiro Mizutani, Masahiko Sakai: Transformation for Refining Unraveled Conditional Term Rewriting Systems. 75-95
• 
  Claudio Sacerdoti Coen: Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I. 97-118
• 
  Mercedes Hidalgo-Herrero, Alberto Verdejo, Yolanda Ortega-Mallén: Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics. 119-137
• 
  Muck van Weerdenburg: An Account of Implementing Applicative Term Rewriting. 139-155

Volume 174, Number 11, July 2007

Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006)

• 
  Myla Archer, Thierry Boy de la Tour, César Muñoz: Preface. 1-2
• 
  Steven Eker, Narciso Martí-Oliet, José Meseguer, Alberto Verdejo: Deduction, Strategies, and Rewriting. 3-25
• 
  Maria Paola Bonacina, Mnacho Echenim: Rewrite-Based Decision Procedures. 27-45
• 
  Florent Kirchner, César A. Muñoz: PVS#: Streamlined Tacticals for PVS. 47-58
• 
  Hongping Lim, Myla Archer: Translation Templates to Support Strategy Development in PVS. 59-79