Multipliers and dividers: Insights on arithmetic circuit verification (extended abstract) -- Global rebuilding of OBDDs avoiding memory requirement maxima -- Generating BDD models for process algebra terms -- Hardware verification using monadic second-order logic -- Verifying safety properties of a class of infinite-state distributed algorithms -- Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving -- CAVEAT: technique and tool for computer aided verification and transformation -- An integration of model checking with automated proof checking -- Automatic datapath abstraction in hardware systems -- Toupie=?-calculus+constraints -- Safety property verification of Esterel programs and applications to telecommunications software -- Methods for Mu-calculus model checking: A tutorial -- Efficient checking of behavioural relations and modal assertions using fixed-point inversion -- It usually works: The temporal logic of stochastic systems -- Local liveness for compositional modeling of fair reactive systems -- Trace theoretic verification of asynchronous circuits using unfoldings -- From duration calculus to linear hybrid automata -- Local model checking for real-time systems -- Algorithmic analysis of nonlinear hybrid systems -- On polynomial-size programs winning finite-state games -- The rabin index and chain automata, with applications to automata and games -- An automata-theoretic approach to fair realizability and synthesis -- Supervisory control of finite state machines -- Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form -- Utilizing symmetry when model checking under fairness assumptions: An automata-theoretic approach -- Augmenting branching temporal logics with existential quantification over atomic propositions -- Modelling asynchrony with a synchronous model -- On the model checking problem for branching time logics and basic parallel processes -- Using formal verification/analysis methods on the critical path in system design: A case study -- Automated analysis of an audio control protocol -- Interactively verifying a simple real-time scheduler -- Verification of real-time systems by successive over and under approximation -- Efficient timing analysis of a class of Petri nets -- Verifying ?-regular properties for a subclass of linear hybrid systems.