## Peter D. Mosses, Mogens Nielsen, Michael I. Schwartzbach

*Proceedings of the Sixth International Joint Conference on Theory and Practice of Software Development*

TAPSOFT CAAP/FASE, 1995.

@proceedings{TAPSOFT-1995, doi = "10.1007/3-540-59293-8", editor = "Peter D. Mosses and Mogens Nielsen and Michael I. Schwartzbach", isbn = "3-540-59293-8", publisher = "{Springer}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Sixth International Joint Conference on Theory and Practice of Software Development}", volume = 915, year = 1995, }

### Contents (61 items)

- TAPSOFT-1995-EhrigM #aspect-oriented #development #process #theory and practice
- A Decade of TAPSOFT: Aspects of Process and Prospects in Theory and Practice of Software Development (HE, BM), pp. 3–24.
- TAPSOFT-1995-Floyd #development #theory and practice
- Theory and Practice of Software Development: Stages in a Debate (CF), pp. 25–41.
- TAPSOFT-1995-Kozen #constraints #set
- Rational Spaces and Set Constraints (DK), pp. 42–61.
- TAPSOFT-1995-GoguenL #development #formal method #social
- Formal Methods and Social Context in Software Development (JAG, L), pp. 62–81.
- TAPSOFT-1995-Gaudel #testing
- Testing Can Be Formal, Too (MCG), pp. 82–96.
- TAPSOFT-1995-Pratt #debugging
- Anatomy of the Pentium Bug (VRP), pp. 97–107.
- TAPSOFT-1995-Pratt95a
- Rational Mechanisms and Natural Mathematics (VRP), pp. 108–122.
- TAPSOFT-1995-Potthoff #finite #first-order #logic
- First-Order Logic on Finite Trees (AP), pp. 125–139.
- TAPSOFT-1995-Salomaa #automaton #decidability #equivalence
- Decidability of Equivalence for Deterministic Synchronized Tree Automata (KS), pp. 140–154.
- TAPSOFT-1995-AndreB #bottom-up #equivalence #problem #transducer
- The Equivalence Problem for Letter-to-Letter Bottom-up Tree Transducers is Solvable (YA, FB), pp. 155–171.
- TAPSOFT-1995-Sangiorgi #calculus #named #symmetry
- Pi-I: A Symmetric Calculus Based on Internal Mobility (DS), pp. 172–186.
- TAPSOFT-1995-Lin #bisimulation #π-calculus
- Complete Inference Systems for Weak Bisimulation Equivalences in the pi-Calculus (HL), pp. 187–201.
- TAPSOFT-1995-AmadioD #higher-order #process #reasoning
- Reasoning about Higher-Order Processes (RMA, MD), pp. 202–216.
- TAPSOFT-1995-LiuW #confluence #process
- Confluence of Processes and Systems of Objects (XL0, DW), pp. 217–231.
- TAPSOFT-1995-Karger #algebra #approach #logic
- An Algebraic Approach to Temporal Logic (BvK), pp. 232–246.
- TAPSOFT-1995-HofmannS #abstraction #behaviour #higher-order #logic #on the
- On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic (MH0, DS), pp. 247–261.
- TAPSOFT-1995-JonssonT #linear #logic #specification
- Assumption/Guarantee Specifications in Linear-Time Temporal Logic (Extended Abstract) (BJ, YKT), pp. 262–276.
- TAPSOFT-1995-Selivanov
- Fine Hierarchy of Regular omega-Languages (VLS), pp. 277–287.
- TAPSOFT-1995-WilkeY #infinity #polynomial #regular expression #word
- Computing the Wadge Degree, the Lifschitz Degree, and the Rabin Index of a Regular Language of Infinite Words in Polynomial Time (TW, HY), pp. 288–302.
- TAPSOFT-1995-Wacrenier #morphism
- Semi-Trace Morphisms and Rational Transductions (PAW), pp. 303–317.
- TAPSOFT-1995-BloomE #axiom
- Nonfinite Axiomatizability of Shuffle Inequalities (SLB, ZÉ), pp. 318–333.
- TAPSOFT-1995-Sassone #on the #petri net
- On the Category of Petri Net Computations (VS), pp. 334–348.
- TAPSOFT-1995-Jancar #petri net #similarity
- High Undecidability of Weak Bisimilarity for Petri Nets (PJ), pp. 349–363.
- TAPSOFT-1995-BadouelBD #algorithm #bound #polynomial #synthesis
- Polynomial Algorithms for the Synthesis of Bounded Nets (EB, LB, PD), pp. 364–378.
- TAPSOFT-1995-Rao #term rewriting
- Semi-Completeness of Hierarchical and Super-Hierarchical Combinations of Term Rewriting Systems (MRKKR), pp. 379–393.
- TAPSOFT-1995-OkuiMI #lazy evaluation
- Lazy Narrowing: Strong Completeness and Eager Variable Elimination (Extended Abstract) (SO, AM, TI), pp. 394–408.
- TAPSOFT-1995-Wagner #algebra #graph grammar #on the #power of
- On the Expressive Power of Algebraic Graph Grammars with Application Conditions (AW), pp. 409–423.
- TAPSOFT-1995-WalickiM #modelling #nondeterminism
- Generated Models and the omega-Rule: The Nondeterministic Case (MW, SM), pp. 424–438.
- TAPSOFT-1995-AcetoI #modelling
- CPO Models for a Class of GSOS Languages (LA, AI), pp. 439–453.
- TAPSOFT-1995-Peron
- Statecharts, Transition Structures and Transformations (AP), pp. 454–468.
- TAPSOFT-1995-AbadiC #calculus #imperative
- An Imperative Object Calculus (MA, LC), pp. 471–485.
- TAPSOFT-1995-KaraliH #composition #logic programming #refinement #semantics
- A Refinement of Import/Export Declarations in Modular Logic Programming and its Semantics (IK, CH), pp. 486–500.
- TAPSOFT-1995-Solberg #analysis #strict
- Strictness and Totality Analysis with Conjunction (KLS), pp. 501–515.
- TAPSOFT-1995-Tip #debugging #slicing
- Generic Techniques for Source-Level Debugging and Dynamic Program Slicing (FT), pp. 516–530.
- TAPSOFT-1995-BertotF #execution #reasoning #specification
- Reasoning with Executable Specifications (YB, RF), pp. 531–545.
- TAPSOFT-1995-KieburtzBBHLOSWZ #generative #specification
- Calculating Software Generators from Solution Specifications (RBK, FB, JMB, JH, JL, DO, TS, LW, TZ), pp. 546–560.
- TAPSOFT-1995-Palsberg #analysis
- Comparing Flow-Based Binding-Time Analyses (JP), pp. 561–574.
- TAPSOFT-1995-Orbaek #question #trust
- Can you Trust your Data? (PØ), pp. 575–589.
- TAPSOFT-1995-NielsonN #concurrent #higher-order
- Static and Dynamic Processor Allocation for Higher-Order Concurrent Languages (HRN, FN), pp. 590–604.
- TAPSOFT-1995-Geser #induction #proving
- Mechanized Inductive Proof of Properties of a Simple Code Optimizer (AG), pp. 605–619.
- TAPSOFT-1995-AndersenM #algebra #case study #process
- Describing a Signal Analyzer in the Process Algebra PMC - A Case Study (HRA, MM), pp. 620–635.
- TAPSOFT-1995-Kleuker #case study #specification #using
- A Gentle Introduction to Specification Engineering Using a Case Study in Telecommunications (SK), pp. 636–650.
- TAPSOFT-1995-SagivRH #analysis #constant #data flow #interprocedural #precise
- Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation (SS, TWR, SH), pp. 651–665.
- TAPSOFT-1995-BlazyF #prototype #specification
- Formal Specification and Prototyping of a Program Specializer (SB, PF), pp. 666–680.
- TAPSOFT-1995-Sands #automation #correctness #program transformation #proving #recursion
- Proving the Correctness of Recursion-Based Automatic Program Transformations (DS), pp. 681–695.
- TAPSOFT-1995-Lano #refinement #specification
- Reactive System Specification and Refinement (KL), pp. 696–710.
- TAPSOFT-1995-BareauCJT #concurrent #distributed
- Measuring Concurrency of Regular Distributed Computations (CB, BC, CJ, RT), pp. 711–725.
- TAPSOFT-1995-Moreau #continuation #parallel
- Non-Speculative and Upward Invocation of Continuations in a Parallel Language (LM0), pp. 726–740.
- TAPSOFT-1995-BertO #model inference #specification
- A Model Inference System for Generic Specification with Application to Code Sharing (DB, CO), pp. 741–755.
- TAPSOFT-1995-Baumeister #algebra #data type
- Relations as Abstract Datatypes: An Institution to Specify Relations between Algebras (HB), pp. 756–771.
- TAPSOFT-1995-Schieferdecker #approach #specification
- Performance-Oriented Formal Specifications - the LotoTis Approach (IS), pp. 772–786.
- TAPSOFT-1995-Guernic #design #named #realtime
- Signal: A Formal Design Environment for Real-Time Systems (PLG), pp. 789–790.
- TAPSOFT-1995-SteffenMC #flexibility
- The META-Frame: An Environment for Flexible Tool Management (BS, TM, AC), pp. 791–792.
- TAPSOFT-1995-MannaBBCCADKLSU #named #proving
- STeP: The Stanford Temporal Prover (ZM, NB, AB, EYC, MC, LdA, HD, AK, JL, HS, TEU), pp. 793–794.
- TAPSOFT-1995-AndersenBNPP #verification
- The HOL-UNITY Verification System (FA, UB, KN, KDP, JSP), pp. 795–796.
- TAPSOFT-1995-SampaioHPUFA #named #programming #proving #term rewriting
- PLATO: A Tool to Assist Programming as Term Rewriting and Therem Proving (AJS, AMH, CTP, CDU, MFF, NCA), pp. 797–798.
- TAPSOFT-1995-Marre #algebra #named #specification #testing
- LOFT: A Tool for Assisting Selection of Test Data Sets from Algebraic Specifications (BM), pp. 799–800.
- TAPSOFT-1995-AstesianoRM #tool support
- The SMoLCS ToolSet (EA, GR, FM), pp. 801–802.
- TAPSOFT-1995-BrandV #asf+sdf #documentation #exclamation #for free #ide #tool support
- The Asf+Sdf Meta-Environment Documentation Tools for Free! (MvdB, EV), pp. 803–804.
- TAPSOFT-1995-B-Core #named
- B-Core: The B-Toolkit Demonstration, pp. 805–806.
- TAPSOFT-1995-GuedesHR #compilation #generative #object-oriented #prototype #semantics
- Object Oriented Semantics Directed Compiler Generation: A Prototype (LCCG, EHH, JLR), pp. 807–808.