| |
| |
| A Decade of TAPSOFT: Aspects of Progress and Prospects in Theory and Practice of Software Development | |
| |
| |
| |
| Theory and Practice of Software Development - Stages in a Debate | |
| |
| |
| |
| Rational Spaces and Set Constraints | |
| |
| |
| |
| Formal Methods and Social Context in Software Development | |
| |
| |
| |
| Testing Can Be Formal, Too | |
| |
| |
| |
| Anatomy of the Pentium Bug | |
| |
| |
| |
| Rational Mechanics and Natural Mathematics | |
| |
| |
| |
| First-Order Logic on Finite Trees | |
| |
| |
| |
| Decidability of Equivalence for Deterministic Synchronized Tree Automata | |
| |
| |
| |
| The Equivalence Problem for Letter-to-Letter Bottom-up Tree Transducers is Solvable | |
| |
| |
| |
| [pi]I: A Symmetric Calculus based on Internal Mobility | |
| |
| |
| |
| Complete Inference Systems for Weak Bisimulation Equivalences in the [pi]-Calculus | |
| |
| |
| |
| Reasoning about Higher-Order Processes | |
| |
| |
| |
| Confluence of Processes and Systems of Objects | |
| |
| |
| |
| An Algebraic Approach to Temporal Logic | |
| |
| |
| |
| On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic | |
| |
| |
| |
| Assumption/Guarantee Specifications in Linear-Time Temporal Logic (Extended Abstract) | |
| |
| |
| |
| Fine Hierarchy of Regular [omega]-Languages | |
| |
| |
| |
| Computing the Wadge Degree, the Lifschitz Degree, and the Rabin Index of a Regular Language of Infinite Words in Polynomial Time | |
| |
| |
| |
| Semi-Trace Morphisms and Rational Transductions | |
| |
| |
| |
| Nonfinite Axiomatizability of Shuffle Inequalities | |
| |
| |
| |
| On the Category of Petri Net Computations | |
| |
| |
| |
| High Undecidability of Weak Bisimilarity for Petri Nets | |
| |
| |
| |
| Polynomial Algorithms for the Synthesis of Bounded Nets | |
| |
| |
| |
| Semi-Completeness of Hierarchical and Super-Hierarchical Combinations of Term Rewriting Systems | |
| |
| |
| |
| Lazy Narrowing: Strong Completeness and Eager Variable Elimination (Extended Abstract) | |
| |
| |
| |
| On the Expressive Power of Algebraic Graph Grammars with Application Conditions | |
| |
| |
| |
| Generated Models and the [omega]-Rule: The Nondeterministic Case | |
| |
| |
| |
| CPO Models for a Class of GSOS Languages | |
| |
| |
| |
| Statecharts, Transition Structures and Transformations | |
| |
| |
| |
| An Imperative Object Calculus | |
| |
| |
| |
| A Refinement of Import/Export Declarations in Modular Logic Programming and Its Semantics | |
| |
| |
| |
| Strictness and Totality Analysis with Conjunction | |
| |
| |
| |
| Generic Techniques for Source-Level Debugging and Dynamic Program Slicing | |
| |
| |
| |
| Reasoning with Executable Specifications | |
| |
| |
| |
| Calculating Software Generators from Solution Specifications | |
| |
| |
| |
| Comparing Flow-Based Binding-Time Analyses | |
| |
| |
| |
| Can you Trust your Data? | |
| |
| |
| |
| Static and Dynamic Processor Allocation for Higher-Order Concurrent Languages | |
| |
| |
| |
| Mechanized Inductive Proof of Properties of a Simple Code Optimizer | |
| |
| |
| |
| Describing a Signal Analyzer in the Process Algebra PMC - A Case Study | |
| |
| |
| |
| A Gentle Introduction to Specification Engineering Using a Case Study in Telecommunications | |
| |
| |
| |
| Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation | |
| |
| |
| |
| Formal Specification and Prototyping of a Program Specializer | |
| |
| |
| |
| Proving the Correctness of Recursion-Based Automatic Program Transformations | |
| |
| |
| |
| Reactive System Specification and Refinement | |
| |
| |
| |
| Measuring Concurrency of Regular Distributed Computations | |
| |
| |
| |
| Non-Speculative and Upward Invocation of Continuations in a Parallel Language | |
| |
| |
| |
| A Model Inference System for Generic Specification with Application to Code Sharing | |
| |
| |
| |
| Relations as Abstract Datatypes: An Institution to Specify Relations Between Algebras | |
| |
| |
| |
| Performance-Oriented Formal Specifications - the LotoTis Approach | |
| |
| |
| |
| Signal: A Formal Design Environment for Real-Time Systems | |
| |
| |
| The META-Frame: An Environment for Flexible Tool Management | |
| |
| |
| |
| STeP: The Stanford Temporal Prover | |
| |
| |
| |
| The HOL-UNITY Verification System | |
| |
| |
| |
| PLATO: A Tool to Assist Programming as Term Rewriting and Theorem Proving | |
| |
| |
| |
| LOFT: A Tool for Assisting Selection of Test Data Sets from Algebraic Specifications | |
| |
| |
| |
| The SMoLCS ToolSet | |
| |
| |
| |
| The ASF+SDF Meta-Environment: Documentation Tools for Free! | |
| |
| |
| |
| The B-Toolkit Demonstration | |
| |
| |
| Object Oriented Semantics Directed Compiler Generation: A Prototype | |
| |
| |
| |
| Author Index | |