Bibliography

[BCCZ99]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. Tools and Algorithms for Construction and Analysis of Systems, In TACAS'99, March 1999.

[CCG+02]

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. Proceedings of Computer Aided Verification (CAV 02), 2002.

[CCGR00]

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker.. International Journal on Software Tools for Technology Transfer (STTT), 2(4), March 2000.

[BCLM+94]

J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401--424, April 1994.

[CGH97]

E. Clarke, O. Grumberg and K. Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design, 10(1):57--71, February 1997.

[CMB90]

O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 365--373, Berlin, June 1990. Springer.

[Dil88]

D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1988.

[EMSS91]

E. Allen Emerson, A. K. Mok, A. Prasad Sistla, and Jai Srinivasan. Quantitative temporal reasoning. In Edmund M. Clarke and Robert P. Kurshan, editors, Proceedings of Computer-Aided Verification (CAV '90), volume 531 of LNCS, pages 136--145, Berlin, Germany, June 1991. Springer.

[McMil92]

K.L. McMillan. The SMV system -- DRAFT. 1992.
Available at http://www.cs.cmu.edu/~modelcheck/smv/smvmanual.r2.2.ps.

[McMil93]

K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.

[Mart85]

A.J. Martin. The design of a self-timed circuit for distributed mutual exclusion. In H. Fuchs and W.H. Freeman, editors, Proceedings of the 1985 Chapel Hill Conference on VLSI, pages 245--260, New York, 1985.

[MOON00]

Moon, Hachtel, Somenzi, Border-Block Tringular Form and Conjunction Schedule in Image Computation, to appear at FMCAD00.

[RAP+95]

R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995.

[Som98]

F. Somenzi. CUDD: CU Decision Diagram package -- release 2.2.0 Department of Electrical and Computer Engineering -- University of Colorado at Boulder, May 1998.

[Vis96]

"VIS: A system for Verification and Synthesis", The VIS Group, In the Proceedings of the 8th International Conference on Computer Aided Verification, p428-432, Springer Lecture Notes in Computer Science, #1102, Edited by R. Alur and T. Henzinger, New Brunswick, NJ, July 1996

Go to the first, previous, next, last section, table of contents.