Hardware and software synthesis, optimization, and verification from Esterel programs.- Manipulation algorithms for K*BMDs.- Combining partial order and symmetry reductions.- Partial model checking with ROBDDs.- Space efficient reachability analysis through use of pseudo-root states.- The reference component of PEP.- A tool to support formal reasoning about computer languages.- The term processor generator Kimwitu.- Graphs in MetaFrame: The unifying power of polymorphism.- A tableau system for linear-TIME temporal logic.- Model-checking for a subclass of event structures.- Real-time logics: Fictitious clock as an abstraction of dense time.- Mosel: A flexible toolset for monadic second-order logic.- A brief introduction to coloured Petri Nets.- Design/CPN — A computer tool for Coloured Petri Nets.- Formal verification of statecharts with instantaneous chain reactions.- Compositional state space generation from Lotos programs.- Syntactic detection of process divergence and non-local choice in message sequence charts.- An automata based verification environment for mobile processes.- Compositional performance analysis.- Incremental development of deadlock-free communicating systems.- Automatic synthesis of specifications from the dynamic observation of reactive programs.- Visual verification of reactive systems.- Theorem prover support for the refinement of stream processing functions.- Integration in PVS: Tables, types, and model checking.- Test generation for intelligent networks using model checking.- Mechanically verified self-stabilizing hierarchical algorithms.- The bounded retransmission protocol must be on time!.