next up previous
Up: NuSMV: a new Symbolic Previous: 5. Results and Future


A. Biere, A. Cimatti, E. Clarke, and Y. Zhu.
Symbolic Model Checking without BDDs.
In Proc. TACAS'99, March 1999.
To appear.

R. K. Brayton et al.
VIS: A system for Verification and Synthesis.
In Proc. of CAV'96. LNCS 1102, Springer-Verlag.

J. Burch, E. Clarke, and D. Long.
Representing Circuits More Efficiently in Symbolic Model Checking.
In Proc. of the 28th ACM/IEEE Design Automation Conference, pages 403-407, Los Alamitos, CA, June 1991. IEEE Computer Society Press.

A. Cimatti, M. Roveri, and P. Traverso.
Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains.
In Proc. of the 15th National Conference on Artificial Intelligence (AAAI-98), Madison, Wisconsin, 1998. AAAI-Press.

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

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

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.

F. Somenzi.
CUDD: CU Decision Diagram package -- release 2.1.2.
Department of Electrical and Computer Engineering -- University of Colorado at Boulder, April 1997.

NuSMV <>