Reflections on Verifying Software with Whiley | SpringerLink
Skip to main content
Springer Nature Link
Log in

Reflections on Verifying Software with Whiley

  • Conference paper
  • First Online:
Formal Techniques for Safety-Critical Systems (FTSCS 2013)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 419))

Abstract

An ongoing challenge for computer science is the development of a tool which automatically verifies that programs meet their specifications, and are free from runtime errors such as divide-by-zero, array out-of-bounds and null dereferences. Several impressive systems have been developed to this end, such as ESC/Java and Spec#, which build on existing programming languages (e.g. Java, C#). Unfortunately, such languages were not designed for this purpose and this significantly hinders the development of practical verification tools for them. For example, soundness of verification in these tools is compromised (e.g. arithmetic overflow is ignored). We have developed a programming language specifically designed for verification, called Whiley, and an accompanying verifying compiler. In this paper, we reflect on a number of challenges we have encountered in developing a practical system.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Hoare, C.A.R.: The verifying compiler: a grand challenge for computing research. JACM 50(1), 63–69 (2003)

    Article  Google Scholar 

  2. King, S.: A program verifier. Ph.D. thesis, Carnegie-Mellon University (1969)

    Google Scholar 

  3. Peter Deutsch, L.: An interactive program verifier. Ph.D. thesis, University of California (1973)

    Google Scholar 

  4. Good, D.I.: Mechanical proofs about computer programs. In: Hoare, C.A.R., Shepherdson, J.C. (eds.) Mathematical Logic and Programming Languages, pp. 55–75. Prentice Hall, Englewood Cliffs (1985)

    Google Scholar 

  5. Luckham, D.C., German, S.M., von Henke, F.W., Karp, R.A., Milne, P.W., Oppen, D.C., Polak, W., Scherlis, W.L.: Stanford pascal verifier user manual. Technical report CS-TR-79-731, Department of Computer Science, Stanford University (1979)

    Google Scholar 

  6. Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research report 159, Compaq Systems Research Center (1998)

    Google Scholar 

  7. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of PLDI, pp. 234–245 (2002)

    Google Scholar 

  8. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55(1–3), 185–208 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  9. Cok, D.R., Kiniry, J.R.: ESC/Java2: uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)

    Google Scholar 

  10. Barnett, M., Rustan, K., Leino, M., Schulte, W.: The Spec# programming system: an overview. Technical report, Microsoft Research (2004)

    Google Scholar 

  11. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27–56 (2004)

    Article  Google Scholar 

  12. Barnett, M., Evan Chang, B.-Y., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Google Scholar 

  13. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)

    Google Scholar 

  14. Rustan, K., Leino, M.: Developing verified programs with Dafny. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, p. 82. Springer, Heidelberg (2012)

    Google Scholar 

  15. The whiley programming language. http://whiley.org

  16. Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238–248. Springer, Heidelberg (2013)

    Google Scholar 

  17. Pearce, D., Noble, J.: Implementing a language with flow-sensitive and structural typing on the JVM. Electron. Notes Theoret. Comput. Sci. 279(1), 47–59 (2011)

    Article  Google Scholar 

  18. Pearce, D.J.: Sound and complete flow typing with unions, intersections and negations. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 335–354. Springer, Heidelberg (2013)

    Google Scholar 

  19. Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358–372. Springer, Heidelberg (2007)

    Google Scholar 

  20. Floyd, R.W.: Assigning meaning to programs. In: Proceedings AMS, vol. 19, pp. 19–31. American Mathematical Society (1967)

    Google Scholar 

  21. Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 576–580 (1969)

    Article  MATH  Google Scholar 

  22. Dijkstra, E.W.: Guarded commands, nondeterminancy and formal derivation of programs. CACM 18, 453–457 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  23. Rountev, A.: Precise identification of side-effect-free methods in Java. In: Proceedings of ICSM, pp. 82–91. IEEE Computer Society (2004)

    Google Scholar 

  24. Sălcianu, A., Rinard, M.: Purity and side effect analysis for Java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 199–215. Springer, Heidelberg (2005)

    Google Scholar 

  25. Mycroft, A.: Programming language design and analysis motivated by hardware evolution. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 18–33. Springer, Heidelberg (2007)

    Google Scholar 

  26. Tobin-Hochstadt, S., Felleisen, M.: Logical types for untyped languages. In: Proceedings of ICFP, pp. 117–128 (2010)

    Google Scholar 

  27. Guha, A., Saftoiu, C., Krishnamurthi, S.: Typing local control and state using flow analysis. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 256–275. Springer, Heidelberg (2011)

    Google Scholar 

  28. Barbanera, F., Dezani-Cian Caglini, M.: Intersection and union types. In: Proceedings of the TACS, pp. 651–674 (1991)

    Google Scholar 

  29. Igarashi, A., Nagira, H.: Union types for object-oriented programming. J. Object Technol. 6(2), 31–52 (2007)

    Article  Google Scholar 

  30. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  31. Hoare, T.: Null references: The billion dollar mistake, presentation at QCon (2009)

    Google Scholar 

  32. Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Proceedings of the OOPSLA, pp. 302–312. ACM Press (2003)

    Google Scholar 

  33. Ekman, T., Hedin, G.: Pluggable checking and inferencing of non-null types for Java. J. Object Technol. 6(9), 455–475 (2007)

    Article  Google Scholar 

  34. Chalin, P., James, P.R.: Non-null references by default in Java: alleviating the nullity annotation burden. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 227–247. Springer, Heidelberg (2007)

    Google Scholar 

  35. Male, C., Pearce, D.J., Potanin, A., Dymnikov, C.: Java bytecode verification for @NonNull types. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 229–244. Springer, Heidelberg (2008)

    Google Scholar 

  36. Hubert, L.: A non-null annotation inference for Java bytecode. In: Proceedings of the PASTE, pp. 36–42. ACM (2008)

    Google Scholar 

  37. ISO/IEC. international standard ISO/IEC 9899, programming languages – C (1990)

    Google Scholar 

  38. Lameed, N., Hendren, L.: Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 22–41. Springer, Heidelberg (2011)

    Google Scholar 

  39. Frade, M.J., Pinto, J.S.: Verification conditions for source-level imperative programs. Comput. Sci. Rev. 5(3), 252–277 (2011)

    Article  Google Scholar 

  40. Gordon, M., Collavizza, H.: Forward with Hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, History of Computing, pp. 101–121. Springer, London (2010)

    Chapter  Google Scholar 

  41. Chadha, R., Plaisted, D.A.: On the mechanical derivation of loop invariants. J. Symbolic Comput. 15(5 & 6), 705–744 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  42. Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119–134. Springer, Heidelberg (2005)

    Google Scholar 

  43. Furia, C.A., Meyer, B.: Inferring loop invariants using postconditions. CoRR, abs/0909.0884 (2009)

    Google Scholar 

  44. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of the TACAS, pp. 337–340, (2008)

    Google Scholar 

  45. Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM 52, 365–473 (2005)

    Article  MathSciNet  Google Scholar 

  46. Leino, K.R.M., Millstein, T.D., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55(1–3), 209–226 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  47. Jager, I., Brumley, D.: Efficient directionless weakest preconditions. Technical Report CMU-CyLab-10-002, Carnegie Mellon University (2010)

    Google Scholar 

  48. Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Google Scholar 

  49. Barnett, M., Rustan M. Leino, K.: Weakest-precondition of unstructured programs. In: Proceedings of the PASTE, pp. 82–87. ACM Press (2005)

    Google Scholar 

  50. Jacobs, B.: Weakest pre-condition reasoning for Java programs with JML annotations. JLAP 58(1–2), 61–88 (2004)

    MATH  MathSciNet  Google Scholar 

  51. Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: a developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  52. Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: Proceedings of the PLDI, pp. 363–374. ACM Press (2009)

    Google Scholar 

  53. Denney, E., Fischer, B.: Explaining verification conditions. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 145–159. Springer, Heidelberg (2008)

    Google Scholar 

Download references

Acknowledgements

This work is supported by the Marsden Fund, administered by the Royal Society of New Zealand.

Author information

Authors and Affiliations

  1. Victoria University of Wellington, Wellington, New Zealand

    David J. Pearce & Lindsay Groves

Authors
  1. David J. Pearce
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lindsay Groves
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David J. Pearce .

Editor information

Editors and Affiliations

  1. AIST, Research Institute for Secure Systems, Amagasaki, Japan

    Cyrille Artho

  2. University of Oslo Department of Informatics, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Pearce, D.J., Groves, L. (2014). Reflections on Verifying Software with Whiley. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2013. Communications in Computer and Information Science, vol 419. Springer, Cham. https://doi.org/10.1007/978-3-319-05416-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-05416-2_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-05415-5

  • Online ISBN: 978-3-319-05416-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation