Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Temporal Logic Framework for Performance Analysis of Architectures of Systems Read chapter Read first chapter

2016 | OriginalPaper | Chapter

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

Authors : Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché

Published in: NASA Formal Methods

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Gray-Box Learning of Serial Compositions of Mealy Machines
next chapter Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Literature
1.
Barnes, J.: Programming in Ada 2012. Cambridge University Press, Cambridge (2014)CrossRef
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)CrossRef
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)CrossRef
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)
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)
6.
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)CrossRef
8.
Boldo, S., Marché, C.: Formal verification of numerical programs: from C annotated programs to mechanical proofs. Math. Comput. Sci. 5, 377–393 (2011)CrossRefMATH
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)
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)CrossRefMATH
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)
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)CrossRef
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)
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)
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)CrossRef
16.
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)
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)CrossRef
19.
Leino, K.R.M., Wüstholz, V.: The Dafny integrated development environment. F-IDE. EPTCS 149, 3–15 (2014)CrossRef
20.
21.
McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)CrossRefMATH
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)CrossRef
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)
24.
Warren, H.S.: Hackers’s Delight. Addison-Wesley, Boston (2003)
Metadata
Title
Specification and Proof of High-Level Functional Properties of Bit-Level Programs
Authors
Clément Fumex
Claire Dross
Jens Gerlach
Claude Marché
Copyright Year
2016
Book
NASA Formal Methods

Print ISBN: 978-3-319-40647-3

Electronic ISBN: 978-3-319-40648-0

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-40648-0_22

Premium Partner

    Image Credits