Advertisement

Specification and Proof of High-Level Functional Properties of Bit-Level Programs

  • Clément Fumex
  • Claire Dross
  • Jens Gerlach
  • Claude MarchéEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9690)

Abstract

In a computer program, basic functionalities may be implemented using bit-wise operations. To formally specify the expected behavior of such a low-level program, it is desirable that the specification should be at a more abstract level. Formally proving that low-level code conforms to a higher-level specification is challenging, because of the gap between the different levels of abstraction. We address this challenge by designing a rich formal theory of fixed-sized bit vectors, which on the one hand allows a user to write abstract specifications close to the human—or mathematical—level of thinking, while on the other hand permits a close connection to decision procedures and tools for bit vectors, as they exist in the context of the Satisfiability Modulo Theory framework. This approach is implemented in the Why3 environment for deductive program verification, and also in its front-end environment SPARK for the development of safety-critical Ada programs. We report on several case studies used to validate our approach.

Keywords

Decision Procedure Formal Verification Proof Obligation Satisfiability Modulo Theory Native Support 
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.

Notes

Acknowledgments

Thanks to Stefan Gerken from Siemens for providing the original implementation of the BitWalker. Thanks to Stefan Berghofer for providing us with an Isabelle/HOL realization of Why3’s bit vector theory. Thanks to Jean-Christophe Filliâtre, Stuart Matthews, Yannick Moy and Mário Pereira for their comments on preliminary versions of this paper.

References

  1. 1.
    Barnes, J.: Programming in Ada 2012. Cambridge University Press, Cambridge (2014)CrossRefGoogle Scholar
  2. 2.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: 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 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  4. 4.
    Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Design Automation Conference. pp. 522–527. ACM (1998)Google Scholar
  5. 5.
    Berry, G.: The foundations of esterel. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 425–454. The MIT Press, Cambridge (2000)Google Scholar
  6. 6.
    Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008). http://alt-ergo.lri.fr/
  7. 7.
    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Let’s verify this with Why3. Int. J. Softw. Tools Technol. Transf. 17(6), 709–727 (2015)CrossRefGoogle Scholar
  8. 8.
    Boldo, S., Marché, C.: Formal verification of numerical programs: from C annotated programs to mechanical proofs. Math. Comput. Sci. 5, 377–393 (2011)CrossRefzbMATHGoogle Scholar
  9. 9.
    Brain, M., Tinelli, C., Ruemmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: ARITH. pp. 160–167 (2015)Google Scholar
  10. 10.
    Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: An abstraction-based decision procedure for bit-vector arithmetic. Int. J. Softw. Tools Technol. Transf. 11(2), 95–104 (2009)CrossRefzbMATHGoogle Scholar
  11. 11.
    Chapman, R., Schanda, F.: Are we there yet? 20 years of industrial theorem proving with SPARK. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 17–26. Springer, Heidelberg (2014)Google Scholar
  12. 12.
    Cyrluk, D., Rueß, H., Möller, O.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg, O. (ed.) Computer Aided Verification. LNCS, vol. 1254, pp. 60–71. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: contract-based modular verification of concurrent C. In: ICSE. pp. 429–430. IEEE Computer Society Press (2009)Google Scholar
  14. 14.
    Dross, C., Fumex, C., Gerlach, J., Marché, C.: High-level functional properties of bit-level programs: Formal specifications and automated proofs. Research Report 8821, Inria (2015)Google Scholar
  15. 15.
    Filliâtre, J.-C.: Verifying two lines of C with Why3: an exercise in program verification. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 83–97. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  16. 16.
    Gerlach, J.: Validation and verification of implementation/code. Technical report D4.3.2, OpenETCS (2015). https://github.com/openETCS/governance/wiki/State-of-Deliverables
  17. 17.
    Kanig, J., Schonberg, E., Dross, C.: Hi-Lite: the convergence of compiler technology and program verification. In: HILT. pp. 27–34. ACM Press (2012)Google Scholar
  18. 18.
    Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Weiß, B.: The 1st verified software competition: experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154–168. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  19. 19.
    Leino, K.R.M., Wüstholz, V.: The Dafny integrated development environment. F-IDE. EPTCS 149, 3–15 (2014)CrossRefGoogle Scholar
  20. 20.
    Lomont, C.: Fast inverse square root. Technical report, Indiana: Purdue University (2003). http://www.lomont.org/Math/Papers/2003/InvSqrt.pdf
  21. 21.
    McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)CrossRefzbMATHGoogle Scholar
  22. 22.
    de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Nguyen, T.M.T.: Taking architecture and compiler into account in formal proofs of numerical programs. Thèse de doctorat, Université Paris-Sud (2012)Google Scholar
  24. 24.
    Warren, H.S.: Hackers’s Delight. Addison-Wesley, Boston (2003)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Clément Fumex
    • 1
    • 2
    • 3
  • Claire Dross
    • 3
  • Jens Gerlach
    • 4
  • Claude Marché
    • 1
    • 2
    Email author
  1. 1.Inria, Université Paris-SaclayPalaiseauFrance
  2. 2.LRI, CNRS & Univ. Paris-SudOrsayFrance
  3. 3.AdaCoreParisFrance
  4. 4.Fraunhofer FOKUSBerlinGermany

Personalised recommendations