| Contents |
What if model checking must be truly symbolic / H. Hungar ... [et al.] -- Automatic verification of the SCI cache coherence protocol / U. stern, D.L. Dill -- Describing and verifying synchronous circuits with the Boyer-Moore theorem prover / L. Pierre -- Problems encountered in the machine-assisted proof of hardware / P. Curzon -- Formally embedding existing high level synthesis algorithms / D. Eisenbiegler, R. Kumar -- Formal design of a class of computers / L.G. Wang, M. Mendler -- Symbolic analysis and verification of CPA descriptions / M.C. McFarland, T.J. Kowalski -- A foundation for formal reuse of hardware / A.C.V. de Melo, H. Barringer -- State enumeration with abstract descriptions of state machines / F. Corella ... [et al.] -- Transforming boolean relations by symbolic encoding / G. Cabodi ... [et al.] -- Design error diagnosis in sequential circuits / A. Wahba, D. Borrione -- Timing analysis of asynchronous circuits using timed automata / O. Maler, A. Pnueli -- Improved probabilistic verification by hash compaction / U. Stern, D.L. Dill -- Formal support for the ELLA hardware description language / H. Barringer, B. Monahan, A. Williams -- Verifying hardware components within JACK / R. De Nicola ... [et al.] -- Language containment of non-deterministic [omega]-automata / S. Taşiran, R. Hojati, R.K. Brayton -- A partial-order approach to the verification of concurrent systems : checking liveness properties / D. Bolignano -- Semantics of a verification-oriented subset of VHDL / D. Déharbe, D. Borrione -- Reasoning about VHDL using operational and observational semantics / K.G.W. Gossens -- A symbolic relation for a subset of VHDL '87 descriptions and its application to symbolic model checking / E. Encrenaz. |
