Algebraic Methodology and Software Technology

Equational logic as a tool.- Teaching mathematics to software engineers.- The role of education and training in the industrial application of formal methods.- Information algebras.- Verification of logic programs with delay declarations.- An introduction to category-based equational logic.- Knowledge based computation.- Order-sorted algebraic specifications with higher-order functions.- Proving the correctness of behavioural implementations.- On the decidability of process equivalences for the ?-calculus.- Detecting isomorphisms of modular specifications with diagrams.- Higher-order narrowing with convergent systems.- Context-free event domains are recognizable.- Encoding natural semantics in Coq.- Mongruences and cofree coalgebras.- Semantic typing for parametric algebraic specifications.- Causality and true concurrency: A data-flow analysis of the Pi-Calculus.- Verification in continuous time by discrete reasoning.- Dynamic matrices and the cost analysis of concurrent programs.- Petri nets, traces, and local model checking.- An algebraic framework for developing and maintaining real-time systems.- Logical foundations for compositional verification and development of concurrent programs in UNITY.- CPO models for infinite term rewriting.- Completeness results for two-sorted metric temporal logics.- On mechanizing proofs within a complete proof system for Unity.- Automated reasoning about parallel algorithms using powerlists.- Representing, verifying and applying software development steps using the PVS system.- An algebraic development technique for information systems.- A framework for machine-assisted user interface verification.- Specification of the Unix file system: A comparative case study.- A Calculus of Countable Broadcasting Systems.- Symbolic timing devices.- An algebraic construction of the well-founded model.- Confluence in concurrent constraint programming.- A generic algebra for data collections based on constructive logic.- Partial order programming (Revisited).- SPIKE: a system for automatic inductive proofs.- SEAMLESS: Knowledge based evolutionary system synthesis.- An object-oriented front-end for deductive databases.- The SuRE programming framework.- A declarative system for multi-database interoperability.- The METAGEN system.