TAPSOFT '95: Theory and Practice of Software Development: 6th International Joint Conference CAAP/FASE, Aarhus, Denmark, May 22 - 26, 1995. Proceedings (Lecture Notes in Computer Science (915))

This volume presents the proceedings of the Sixth International Joint Conference on the Theory and Practice of Software Engineering, TAPSOFT '95, held in Aarhus, Denmark in May 1995. TAPSOFT '95 celebrates the 10th anniversary of this conference series started in Berlin in 1985 to bring together theoretical computer scientists and software engineers (researchers and practitioners) with a view to discussing how formal methods can usefully be applied in software development. The volume contains seven invited papers, among them one by Vaugham Pratt on the recently revealed bug in the Pentium chip, and 44 revised full papers selected from a total of 147 submissions. In addition the TAPSOFT '95 proceedings contains 10 tool descriptions. A decade of TAPSOFT....Pages 1-24 Theory and practice of software development....Pages 25-41 Rational spaces and set constraints....Pages 42-61 Formal methods and social context in software development....Pages 62-81 Testing can be formal, too....Pages 82-96 Anatomy of the Pentium bug....Pages 97-107 Rational mechanics and natural mathematics....Pages 108-122 First-order logic on finite trees....Pages 123-139 Decidability of equivalence for deterministic synchronized tree automata....Pages 140-154 The equivalence problem for letter-to-letter bottom-up tree transducers is solvable....Pages 155-171 πI: A symmetric calculus based on internal mobility....Pages 172-186 Complete inference systems for weak bisimulation equivalences in the π-calculus....Pages 187-201 Reasoning about higher-order processes....Pages 202-216 Confluence of processes and systems of objects....Pages 217-231 An algebraic approach to temporal logic....Pages 232-246 On behavioural abstraction and behavioural satisfaction in higher-order logic....Pages 247-261 Assumption/guarantee specifications in linear-time temporal logic (extended abstract)....Pages 262-276 Fine hierarchy of regular ω -languages....Pages 277-287 Computing the Wadge degree, the Lifschitz degree, and the Rabin index of a regular language of infinite words in polynomial time....Pages 288-302 Semi-trace morphisms and rational transductions....Pages 303-317 Nonfinite axiomatizability of shuffle inequalities....Pages 318-333 On the category of Petri net computations....Pages 334-348 High undecidability of weak bisimilarity for Petri nets....Pages 349-363 Polynomial algorithms for the synthesis of bounded nets....Pages 364-378 Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems....Pages 379-393 Lazy narrowing: Strong completeness and eager variable elimination (extended abstract)....Pages 394-408 On the expressive power of algebraic graph grammars with application conditions....Pages 409-423 Generated models and the ω-rule: The nondeterministic case....Pages 424-438 CPO models for a class of GSOS languages....Pages 439-453 Statecharts, transition structures and transformations....Pages 454-468 An imperative object calculus....Pages 469-485 A refinement of import/export declarations in modular logic programming and its semantics....Pages 486-500 Strictness and totality analysis with conjunction....Pages 501-515 Generic techniques for source-level debugging and dynamic program slicing....Pages 516-530 Reasoning with executable specifications....Pages 531-545 Calculating software generators from solution specifications....Pages 546-560 Comparing flow-based binding-time analyses....Pages 561-574 Can you trust your data....Pages 575-589 Static and dynamic processor allocation for higher-order concurrent languages....Pages 590-604 Mechanized inductive proof of properties of a simple code optimizer....Pages 605-619 Describing a Signal Analyzer in the process algebra PMC — A case study....Pages 620-635 A gentle introduction to specification engineering using a case study in telecommunications....Pages 636-650 Precise interprocedural dataflow analysis with applications to constant propagation....Pages 651-665 Formal specification and prototyping of a program specializer....Pages 666-680 Proving the correctness of recursion-based automatic program transformations....Pages 681-695 Reactive system specification and refinement....Pages 696-710 Measuring concurrency of regular distributed computations....Pages 711-725 Non-speculative and upward invocation of continuations in a parallel language....Pages 726-740 A model inference system for generic specification with application to code sharing....Pages 741-755 Relations as abstract datatypes: An institution to specify relations between algebras....Pages 756-771 Performance-oriented formal specifications — the LotoTis approach....Pages 772-786 Signal: A formal design environment for real-time systems....Pages 787-790 The META-Frame: An environment for flexible tool management....Pages 791-792 STeP: The Stanford Temporal Prover....Pages 793-794 The HOL-UNITY verification system....Pages 795-796 PLATO: A tool to assist programming as term rewriting and theorem proving....Pages 797-798 LOFT: A tool for assisting selection of test data sets from algebraic specifications....Pages 799-800 The SMoLCS ToolSet....Pages 801-802 The Asf+Sdf Meta-environment documentation tools for free....Pages 803-804 The B-Toolkit demonstration....Pages 805-806 Object Oriented Semantics Directed Compiler Generation: A prototype....Pages 807-808 Theoretical computer scientists and software engineers (researchers and practitioners) discuss how formal methods can usefully be applied in software development. These proceedings of the TAPSOFT '95 conference also contain 44 revised papers and 10 tool descriptions. The idea to have a joint conference on theory and practice of software development was bom following the offer to organize the 1985 Colloquium on Trees in Algebra and Programming (CAAP) in Berlin.