Better verification through symmetry

S. Aggarwal, R.P. Kurshan, and K. Sabnani, ?A calculus for protocol specification and validation,?Protocol Specification, Testing, and Verification, Vol. 3, pp. 19?34, 1983.

J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, ?Symbolic model checking: 1020 states and beyond,?Proc. 5th Ann. IEEE Symp. on Logic in Computer Science, pp. 428?439, 1990.

K.M. Chandy and J. Misra,Parallel Program Design?A Foundation, Addison-Wesley, 1988.

E.M. Clarke, E.A. Emerson, and A.P. Sistla, ?Automatic verification of finite-state concurrent systems using temporal logic specifications,?ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, 1986.

E.M. Clarke, T. Filkorn, and S. Jha, ?Exploiting symmetry in temporal logic model checking,?5th International Conference on Computer-Aided Verification, pp. 450?462, June 1993.

O. Coudert, C. Berthet, and J.C. Madre, ?Verification of synchronous sequential machines based on symbolic execution,?Automatic Verification Methods for Finite State Systems, pp. 365?373, 1989.

D.L. Dill, A.J. Drexler, A.J. Hu, and C.H. Yang, ?Protocol verification as a hardware design aid,?Proc. IEEE Int. Conf. on Computer Design: VLSI in Computers and Processors, pp. 522?525, 1992.

C. Ebeling, ?GeminiII: A second generation layout validation program,?IEEE/ACM Int. Conf. on Computer-Aided Design, pp. 322?325, 1988.

E.A. Emerson and A.P. Sistla, ?Symmetry and model checking,?5th International Conference on Computer-Aided Verification, pp. 463?478, June 1993.

G.J. Holzmann,Automated Protocol Validation in Argos, Assertion Proving and Scatter Searching, Computer Science Press, pp. 163?188, 1987.

P. Huber, A.M. Jensen, L.O. Jepsen, and K. Jensen, ?Towards reachability trees for high-level Petri nets,?Advances on Petri Nets, pp. 215?233, 1984.

C.N. Ip and D.L. Dill, ?Better verification through symmetry,?Proc. 11th Int. Symp. on Computer Hardware Description Languages and Their Application, pp. 97?111, April 1993.

C.N. Ip and D.L. Dill, ?Efficient verification of symmetric concurrent systems,?IEEE International Conference on Computer Design: VLSI in Computers and Processors, Cambridge, MA, pp. 230?234, October 3?6, 1993.

D. Lenoski, J. Laudon, K. Gharachorloo, A. Gupta, and J. Hennessy, ?The directory-based cache coherence protocol for the DASH multiprocessor,?Proc. 17th Int. Symp. on Computer Architercture, pp. 148?159, 1990.

D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M. Lam, ?The Stanford DASH multiprocessor,?Computer, Vol. 25, No. 3, pp. 63?79, 1992.

B.D. Lubachevsky, ?An approach to automating the verification of compact parallel coordination programs, I,?Acta Informatica, Vol. 21, No. 2, pp. 125?169, 1984.

J.M. Mellor-Crummey and M.L. Scott, ?Algorithms for scalable synchronization on shared-memory multiprocessors,?ACM Transactions on Computer Systems, Vol. 9, No. 1, pp. 21?65, 1991.

H.B. Mittal, ?A fast backtrack algorithm for graph isomorphism,?Information Processing Letters, Vol. 29, pp. 105?110, 1988.

G.L.Peterson, ?Myths about the mutual exclusion problem,?Information Processing Letters, Vol. 12, No. 3, pp. 105?110, 1981.

P.H. Starke, ?Reachability analysis of petri nets using symmetries,?Systems Analysis?Modelling?Simulation, Vol. 8, No. 4/5, pp. 293?303, 1991.

H.J. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, ?Implicit state enumeration of finite state machines using BDDs,?IEEE Int. Conf. on Computer-Aided Design, pp. 130?133, 1990.

P. Wolper, ?Expressing interesting properties of programs,?13th Annual ACM Symp. on Principles of Programming Languages, 1986.

P. Zafiropulo, C.H. West, H. Rudin, D.D. Cowan, and D. Brand, ?Towards analyzing and synthesizing protocols,?IEEE Transactions on Communications, Vol. COM-28, No. 4, 1980.