Advertisement

SVISS: Symbolic Verification of Symmetric Systems

  • Thomas Wahl
  • Nicolas Blanc
  • E. Allen Emerson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)

Abstract

Sviss is a flexible platform for incorporating efficient symmetry reduction into symbolic model checking. The tool comes with an extensive C++ library for system modeling using BDDs and a rich CTL-based model checking engine. Applications range from communication protocols to computer hardware and multi-threaded software. We believe Sviss to be the first symbolic tool to exploit symmetry in concurrent device-driver verification, which is vital in operating system design.

References

  1. 1.
    Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)Google Scholar
  2. 2.
    Barner, S., Grumberg, O.: Combining symmetry reduction and Under Approximation for symbolic model checking. In: FMSD 2005 (2005)Google Scholar
  3. 3.
    Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: FMSD 1996 (1996)Google Scholar
  4. 4.
    Emerson, E.A., Trefler, R.J., Wahl, T.: Reducing Model Checking of the Few to the One. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 94–113. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005)Google Scholar
  6. 6.
    Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, Springer, Heidelberg (2004)Google Scholar
  7. 7.
    Melton, R., Dill, D.L.: Murϕ Annotated Reference Manual, rel. 3.1., http://verify.stanford.edu/dill/murphi.html
  8. 8.
    Sistla, A.P., Gyuris, V., Emerson, E.A.: Smc: a symmetry-based model checker for verification of safety and liveness properties. In: ACM ToSEM 2000 (2000)Google Scholar
  9. 9.
    Somenzi, F.: The CU Decision Diagram Package, release 2.3.1, University of Colorado at Boulder, http://vlsi.colorado.edu/~fabio/CUDD/.
  10. 10.
    Wang, F., Schmidt, K., Yu, F., Huang, G.-D., Wang, B.-Y.: Bdd-based safety-analysis of concurrent software with pointer data structures using graph automorphism symmetry reduction. In: IEEE ToSE 2004 (2004)Google Scholar
  11. 11.
    Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent linux device drivers. In: ASE 2007 (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Thomas Wahl
    • 1
  • Nicolas Blanc
    • 1
  • E. Allen Emerson
    • 2
  1. 1.Computer Systems InstituteETH ZurichSwitzerland
  2. 2.Department of Computer SciencesThe University of Texas at AustinUSA

Personalised recommendations