TAPSOFT ’95: Theory and Practice of Software Development: 6th International Joint Conference CAAP/FASE Aarhus, Denmark, May 22–26, 1995 Proceedings

Hartmut Ehrig, Bernd Mahr (auth.), Peter D. Mosses, Mogens Nielsen, Michael I. Schwartzbach (eds.)3540592938, 9783540592938

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.

---

Table of contents :
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