Advertisement

Incremental Benchmarks for Software Verification Tools and Techniques

  • Bruce W. Weide
  • Murali Sitaraman
  • Heather K. Harton
  • Bruce Adcock
  • Paolo Bucci
  • Derek Bronish
  • Wayne D. Heym
  • Jason Kirschenbaum
  • David Frazier
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)

Abstract

This paper proposes an initial catalog of easy-to-state, relatively simple, and incrementally more and more challenging benchmark problems for the Verified Software Initiative. These benchmarks support assessment of verification tools and techniques to prove total correctness of functionality of sequential object-based and object-oriented software. The problems are designed to help evaluate the state-of-the-art and the pace of progress toward verified software in the near term, and in this sense, they are just the beginning. They will allow researchers to illustrate and explain how proposed tools and techniques deal with known pitfalls and well-understood issues, as well as how they can be used to discover and attack new ones. Unlike currently available benchmarks based on “real-world” software systems, the proposed challenge problems are expected to be amenable to “push-button” verification that leverages current technology.

Keywords

Benchmark Problem Verification System Proof Rule Abstract Data Type Problem Requirement 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    ABZ call for papers on the POSIX pilot project in the grand challenge (viewed April 27, 2008), http://www.abz2008.org
  2. 2.
    Pacemaker formal methods challenge (viewed April 27, 2008), http://www.cas.mcmaster.ca/sqrl/pacemaker.htm
  3. 3.
    Stepney, S., Cooper, D., Woodcock, J.: An electronic purse: specification, refinement, and proof. PRG Technical Monograph PRG-126 (2000), 231 pp. (viewed April 27, 2008), http://web2.comlab.ox.ac.uk/oucl/publications/monos/prg-126.html
  4. 4.
    Woodcock, J., Banach, R.: The verification grand challenge. Journal of Universal Computer Science 13(5), 661–668 (2007)Google Scholar
  5. 5.
    Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: Fifth IEEE Intl. Conf. on Software Engineering and Formal Methods, pp. 47–58. IEEE, Los Alamitos (2007)CrossRefGoogle Scholar
  6. 6.
    Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Formal Aspects of Computing 20(1), 41–59 (2007)CrossRefGoogle Scholar
  7. 7.
  8. 8.
    Bicarregui, J.C., Hoare, C.A.R., Woodcock, J.C.P.: The verified software repository: a step towards the verifying compiler. Formal Aspects of Computing 18(2), 143–151 (2006)zbMATHCrossRefGoogle Scholar
  9. 9.
    Ancient Egyptian multiplication (viewed April 27, 2008), http://en.wikipedia.org/wiki/Ancient_Egyptian_multiplication
  10. 10.
    Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  11. 11.
    Bloch, J.: Extra, extra – read all about it: nearly all binary searches and mergesorts are broken (2006) (viewed 27 April 2008), http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html
  12. 12.
    Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for queues with integer constraints. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 225–237. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf 1(4), 271–281 (1972)zbMATHCrossRefGoogle Scholar
  14. 14.
    Sitaraman, M., Weide, B.W., Ogden, W.F.: On the practical need for abstraction relations to verify abstract data type representations. IEEE Transactions on Software Engineering 23(3), 157–170 (1997)CrossRefGoogle Scholar
  15. 15.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proc. 17th Annual IEEE Symp. on Logic in Computer Science, pp. 55–74. IEEE, Los Alamitos (2002)CrossRefGoogle Scholar
  16. 16.
    Kulczycki, G.: Direct Reasoning. Dept. of Computer Science, Ph.D. thesis, ClemsonUniversity, Clemson, SC (2004)Google Scholar
  17. 17.
    Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: ACM Conference on Programming Language Design and Implementation, pp. 349–361. ACM Press, New York (2008)Google Scholar
  18. 18.
    Challenge problem: iterator specification (viewed April 27, 2008), http://www.eecs.ucf.edu/~leavens/SAVCBS/2006/challenge.shtml
  19. 19.
    Leavens, G., (ed.): SAVCBS 2006 Proceedings: Specification and Verification of Component-Based Systems (viewed April 27, 2008), http://www.eecs.ucf.edu/~leavens/SAVCBS/2006/SAVCBS06-proceedings.pdf
  20. 20.
    Booch, G.: Software components with Ada, Benjamin Cummings, Redwood City, CA (1987)Google Scholar
  21. 21.
    Weide, B.W., Edwards, S.H., Harms, D.E., Lamb, D.A.: Design and specification of iterators using the swapping paradigm. IEEE Transactions on Software Engineering 20(8), 631–643 (1994)CrossRefGoogle Scholar
  22. 22.
    Edwards, S.H., Heym, W.D., Long, T.J., Sitaraman, M., Weide, B.W.: Specifying components in RESOLVE. Software Engineering Notes 19(4), 29–39 (1994)CrossRefGoogle Scholar
  23. 23.
    Bucci, P., Hollingsworth, J.E., Krone, J., Weide, B.W.: Implementing components in RESOLVE. Software Engineering Notes 19(4), 40–52 (1994)CrossRefGoogle Scholar
  24. 24.
    Kulczycki, G., Sitaraman, M., Yasmin, N., Roche, K.: Formal specification. In: Encyc. of Computer Science and Engineering. John Wiley & Sons, Chichester (to appear, 2008)Google Scholar
  25. 25.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  26. 26.
    Krone, J.: The Role of Verification in Software Reusability. Ph.D. dissertation, Dept. of Comp. and Inf. Science, Ohio State Univ., Columbus, OH (1988)Google Scholar
  27. 27.
    Harton, H., Krone, J., Sitaraman, M.: Formal program verification. In: Encyc. of Computer Science and Engineering. John Wiley & Sons, Chichester (to appear, 2008)Google Scholar
  28. 28.
    Heym, W.D.: Computer Program Verification: Improvements for Human Reasoning. Ph.D. dissertation, Dept. of Comp. and Inf. Sci., Ohio State Univ., Columbus, OH (1995)Google Scholar
  29. 29.
    Sitaraman, M., Atkinson, S., Kulczycki, G., Weide, B.W., Long, T.J., Bucci, P., Heym, W.D., Pike, S., Hollingsworth, J.E.: Reasoning about software-component behavior. In: Frakes, W.B. (ed.) ICSR 2000. LNCS, vol. 1844, pp. 266–283. Springer, Heidelberg (2000)Google Scholar
  30. 30.
    Zhang, J.: Program verification in the small. In: Proc. First Asian Working Conf. on Verified Software, UNU/IIST Report #348, pp. 83–84 (2006)Google Scholar
  31. 31.
  32. 32.
    RESOLVE/C++ Catalog, AT/Stack/Kernel.h (viewed July 15, 2008), http://www.cse.ohio-state.edu/sce/rcpp/RESOLVE_Catalog-HTML/AT/Stack/Kernel.html

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Bruce W. Weide
    • 1
  • Murali Sitaraman
    • 2
  • Heather K. Harton
    • 2
  • Bruce Adcock
    • 1
  • Paolo Bucci
    • 1
  • Derek Bronish
    • 1
  • Wayne D. Heym
    • 1
  • Jason Kirschenbaum
    • 1
  • David Frazier
    • 2
  1. 1.The Ohio State UniversityColumbusUSA
  2. 2.Clemson UniversityClemsonUSA

Personalised recommendations