Early fault detection tools.- Kleene algebra with tests and commutativity conditions.- Managing proofs.- An analyzer for message sequence charts.- Relation-algebraic analysis of Petri nets with RELVIEW.- Efficient search as a means of executing specifications.- An improvement of McMillan's unfolding algorithm.- Efficient local model-checking for fragments of the modal ?-calculus.- Test generation with inputs, outputs, and quiescence.- Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR.- Automatic compositional verification of some Security properties.- Permutable agents in process algebras.- Strategy construction in infinite games with Streett and Rabin chain winning conditions.- Timed Condition/Event systems: A framework for modular discrete models of chemical plants and verification of their real-time discrete control.- Formal verification of a partial-order reduction technique for model checking.- Fully automatic verification and error detection for parameterized iterative sequential circuits.- Priorities for modeling and verifying distributed systems.- Games and modal mu-calculus.- Generic system support for deductive program development.- Extending promela and spin for real time.- Reactive EFSMs — Reactive Promela/RSPIN.- Probabilistic duration automata for analyzing real-time systems.- The Concurrency Factory software development environment.- The Fc2Tools set (tool demonstration).- PEP — more than a Petri Net tool.- Rapid prototyping for an assertional specification language.- cTc — A tool supporting the construction of cTLA-Specifications.- A tool for proving invariance properties of concurrent systems automatically.- Using the constraint language toupie for “Software Cost Reduction” specification analysis.- A constraint-oriented Service Creation Environment.- DFA&OPT-MetaFrame: A tool kit for program analysis and optimization.- A construction and analysis tool based on the stochastic process algebra TIPP.- Uppaal in 1995.