Advertisement

Making Whiley Boogie!

  • Mark UttingEmail author
  • David J. Pearce
  • Lindsay Groves
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

Abstract

The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#, ESC/Java, SPARK Ada, and Whiley attempt to seamlessly integrate specification and verification into a programming language, in a similar way to type checking. A common integration approach is to generate verification conditions that are handed off to an automated theorem prover. This provides a nice separation of concerns, and allows different theorem provers to be used interchangeably. However, generating verification conditions is still a difficult undertaking and the use of more “high-level” intermediate verification languages has become common-place. In particular, Boogie provides a widely used and understood intermediate verification language. A common difficulty is the potential for an impedance mismatch between the source language and the intermediate verification language. In this paper, we explore the use of Boogie as an intermediate verification language for verifying programs in Whiley. This is noteworthy because the Whiley language has (amongst other things) a rich type system with considerable potential for an impedance mismatch. We report that, whilst a naive translation to Boogie is unsatisfactory, a more abstract encoding is surprisingly effective.

Keywords

Whiley Boogie Verifying compiler Intermediate verification language Semantic translation Impedance mismatch 

References

  1. 1.
    Ameri, M., Furia, C.A.: Why just Boogie? In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 79–95. Springer, Cham (2016). doi: 10.1007/978-3-319-33693-0_6 CrossRefGoogle Scholar
  2. 2.
    Arlt, S., Rümmer, P., Schäf, M.: Joogie: from Java through Jimple to Boogie. In: Proceedings of SOAP (2013)Google Scholar
  3. 3.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). doi: 10.1007/11804192_17 CrossRefGoogle Scholar
  4. 4.
    Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. CACM 54(6), 81–91 (2011)CrossRefGoogle Scholar
  5. 5.
    Betts, A., Chong, N., Donaldson, A.F., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: Proceedings of the OOPSLA, pp. 113–132. ACM Press (2012)Google Scholar
  6. 6.
    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Workshop on Intermediate Verification Languages (2011)Google Scholar
  7. 7.
    Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-03359-9_2 CrossRefGoogle Scholar
  8. 8.
    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). doi: 10.1007/978-3-540-30569-9_6 CrossRefGoogle Scholar
  9. 9.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM 52(3), 365–473 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    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
  11. 11.
    Dijkstra, E.W.: Guarded commands, nondeterminancy and formal derivation of programs. CACM 18, 453–457 (1975)CrossRefzbMATHGoogle Scholar
  12. 12.
    Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006). doi: 10.1007/11817963_11 CrossRefGoogle Scholar
  13. 13.
    Filliâtre, J., Paskevich, A.: Why3 – where programs meet provers. In: Proceedings of ESOP, pp. 125–128 (2013)Google Scholar
  14. 14.
    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
  15. 15.
    Hoare, C.: The verifying compiler: a grand challenge for computing research. JACM 50(1), 63–69 (2003)CrossRefzbMATHGoogle Scholar
  16. 16.
    Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-20398-5_4 CrossRefGoogle Scholar
  17. 17.
    Leino, K.R.M.: Ecstatic: an object-oriented programming language with an axiomatic semantics. In: Workshop on Foundations of Object-Oriented Languages (FOOL 4) (1997)Google Scholar
  18. 18.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-17511-4_20 CrossRefGoogle Scholar
  19. 19.
    Leino, K.R.M.: Program proving using intermediate verification languages (IVLs) like Boogie and Why3. In: Proceedings of HILT, pp. 25–26 (2012)Google Scholar
  20. 20.
    McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)CrossRefzbMATHGoogle Scholar
  21. 21.
    Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  22. 22.
    Moura, L., Bjørner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-73595-3_13 CrossRefGoogle Scholar
  23. 23.
    Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49122-5_2 CrossRefGoogle Scholar
  24. 24.
    Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. JACM 27, 356–364 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    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). doi: 10.1007/978-3-642-35873-9_21 CrossRefGoogle Scholar
  26. 26.
    Pearce, D.J., Groves, L.: Designing a verifying compiler: lessons learned from developing Whiley. Sci. Comput. Program. 113, 191–220 (2015)CrossRefGoogle Scholar
  27. 27.
    Robison, P.J., Staples, J.: Formalizing a hierarchical structure of practical mathematical reasoning. J. Logic Comput. 3(1), 47–61 (1993). http://dx.doi.org/10.1093/logcom/3.1.47 MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Segal, L., Chalin, P.: A comparison of intermediate verification languages: Boogie and Sireum/Pilar. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 130–145. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-27705-4_11 CrossRefGoogle Scholar
  29. 29.
    The SMT-LIB standard: Version 2.0Google Scholar
  30. 30.
    The Whiley programming language. http://whiley.org

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.University of the Sunshine CoastSippy DownsAustralia
  2. 2.Victoria University of WellingtonWellingtonNew Zealand

Personalised recommendations