External Links

    Journal: Electronic Notes in Theoretical Computer Science

    Volume 174, Issue 9

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

    Volume 174, Issue 8

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

    Volume 174, Issue 7

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

    Volume 174, Issue 6

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

    Volume 174, Issue 5

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

    Volume 174, Issue 4

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

    Volume 174, Issue 3

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

    Volume 174, Issue 2

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

    Volume 174, Issue 11

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

    Volume 174, Issue 10

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

    Volume 174, Issue 1

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