TAPSOFT'97: Theory and Practice of Software Development

Theoretical Computer Science and software science: The past, the present and the future (position paper).- Future trends of TAPSOFT.- New challenges for theoretical computer science.- What does the future hold for theoretical computer science?.- Automata theory on trees and partial orders.- A theory of testing for timed automata.- Conservative extensions, interpretations between theories and all that!.- Specification and proof in membership equational logic.- Formalism and method.- CoFI: The common framework initiative for algebraic specification and development.- Logicality of conditional rewrite systems.- Simulating forward-branching systems with constructor systems.- Reliable generalized and context dependent commutation relations.- Word-into-Trees Transducers with bounded difference.- Generalized quantitative temporal reasoning: An automata-theoretic approach.- The Railroad Crossing Problem: Towards semantics of timed algorithms and their model checking in high level languages.- Model checking through symbolic reachability graph.- Optimal implementation of wait-free binary relations.- Relative undecidability in the termination hierarchy of single rewrite rules.- Termination proofs using gpo ordering constraints.- Automatically proving termination where simplification orderings fail.- Generating efficient, terminating logic programs.- Modal characterization of weak bisimulation for higher-order processes.- Formats of ordered SOS rules with silent actions.- A uniform syntactical method for proving coinduction principles in ?-calculi.- A labelled transition system for ??-calculus.- Set operations for recurrent term schematizations.- Inclusion constraints over non-empty sets of trees.- Grid structures and undecidable constraint theories.- Predicative functional recurrence and poly-space.- On the complexity of function pointer may-alias analysis.- Maximum packing for biconnected outerplanar graphs.- Synchronization of a line of identical processors at a given time.- An algorithm for the solution of tree equations.- E-unification by means of tree tuple synchronized grammars.- Linear interpolation for the higher-order matching problem.- A semantic framework for functional logic programming with algebraic polymorphic types.- Subtyping constraints for incomplete objects.- Partializing stone spaces using SFP domains.- Let-polymorphism and eager type schemes.- Semantics of architectural connectors.- Protective interface specifications.- Specifying complex and structured systems with Evolving Algebras.- A comparison of modular verification techniques.- A compositional proof of a real-time mutual exclusion protocol.- Traces of I/O-automata in Isabelle/HOLCF.- Reactive types.- A type-based approach to program security.- An applicative module calculus.- Compositional specification of embedded systems with Statecharts.- Verification of message sequence charts via template matching.- Probabilistic lossy channel systems.- A logic of object-oriented programs.- Auxiliary variables and recursive procedures.- Locality based Linda: Programming with explicit localities.- A syntactic theory of dynamic binding.- A unified framework for binding-time analysis.- A typed intermediate language for flow-directed compilation.- Action refinement as an implementation relation.- Behaviour-refinement of coalgebraic specifications with coinductive correctness proofs.- COMPASS: A comprehensible assertion method.- Using LOTOS patterns to characterize architectural styles.- Automating formal specification-based testing.- TYPELAB: An environment for modular program development.- TAS and IsaWin: Generic interfaces for transformational program development and theorem proving.- Proving system correctness with KIV.- A new proof-manager and graphic interface for the Larch Prover.- A web-based animator for object specifications in a persistent environment.- Publishing formal specifications in Z notation on world wide web.- DOSFOP — A documentation tool for the algebraic programming language Opal.- AG: A set of maple packages for symbolic computing of automata and semigroups.