Article

Sviss: symbolic verification of symmetric systems

Authors:

TACAS'08/ETAPS'08: Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems

Pages 459 - 462

Published: 29 March 2008 Publication History

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 CTLbased 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]

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]

Barner, S., Grumberg, O.: Combining symmetry reduction and Under Approximation for symbolic model checking. In: FMSD 2005 (2005).

Digital Library

Google Scholar

[3]

Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: FMSD 1996 (1996).

Digital Library

Google Scholar

[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).

Digital Library

Google Scholar

[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).

Digital Library

Google Scholar

[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]

Melton, R., Dill, D.L.: Murϕ Annotated Reference Manual, rel. 3.1., http://verify.stanford.edu/dill/murphi.html

Google Scholar

[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).

Digital Library

Google Scholar

[9]

Somenzi, F.: The CU Decision Diagram Package, release 2.3.1, University of Colorado at Boulder, http://vlsi.colorado.edu/~fabio/CUDD/.

Google Scholar

[10]

Wang, F., Schmidt, K., Yu, F., Huang, G.-D., Wang, B.-Y.: Bdd-based safetyanalysis of concurrent software with pointer data structures using graph automorphism symmetry reduction. In: IEEE ToSE 2004 (2004).

Digital Library

Google Scholar

[11]

Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent linux device drivers. In: ASE 2007 (2007).

Digital Library

Google Scholar

Index Terms

Sviss: symbolic verification of symmetric systems
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking

Index terms have been assigned to the content through auto-classification.

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

TACAS'08/ETAPS'08: Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems

March 2008

518 pages

ISBN:3540787992

Editors:
C. R. Ramakrishnan
Stony Brook University, Department of Computer Science, Stony Brook, NY
,
Jakob Rehof
Universität Dortmund, Fachbereich Informatik, Dortmund, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 29 March 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

0
Total Citations
1
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Sep 2024

Other Metrics

View Author Metrics

Citations

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Index Terms

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

Formal verification of ASMs using MDGs

Transition predicate abstraction and fair termination

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

View options

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations