Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Functional dependencies of C functions via weakest pre-conditions

  • VSTTE 2009-2010
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Barnett, M., Chang, B.Y., DeLine, R., Jacobs, B., Leino, K.: Boogie: A modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects, LNCS, vol. 4111, pp. 364–387. Springer, Berlin (2005)

  2. Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language Preliminary design. http://frama-c.com/downloads/acsl-1.4.pdf (2008)

  3. Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Constructions. Lecture Notes in Computer Science, vol. 1837, pp. 102–126. Springer, Berlin (2000)

  4. Burdy L., Cheon Y., Cok D., Ernst M., Kiniry J., Leavens G.T., Leino K.R.M., Poll E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212–232 (2005)

    Article  Google Scholar 

  5. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Footprint analysis: a shape analysis that discovers preconditions. In: Static Analysis Symposium (SAS). LNCS, vol. 4634 (2007)

  6. Cartwright, R., Oppen, D.: Unrestricted Procedure Calls in Hoare’s Logic. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (POPL). pp. 131–140 (1978)

  7. CENELEC: CENELEC 50128—Railway applications—Communication, signalling and processing systems—Software for railway control and protection systems (2001)

  8. Clarke E.M., Grumberg O., Peled D.A.: Model checking. MIT Press, Massachusetts (1999)

    Google Scholar 

  9. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (POPL). pp. 269–282 (1979)

  10. Cuoq, P., Prevosto, V.: Frama-C’s value analysis manual. http://frama-c.com/download/frama-c-value-analysis.pdf (2011)

  11. Filliâtre, J.C.: Preuve de programmes impératifs en théorie des types. Thèse de doctorat, Université Paris-Sud. http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz (1999)

  12. Filliâtre, J.C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud. http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz (2003)

  13. Frama-C home page. http://frama-c.com/

  14. Gries D., Levin G.: Assignment and procedure call proof rules. ACM TOPLAS 2(4), 564–579 (1980)

    Article  MATH  Google Scholar 

  15. Hackett, B., Das, M., Wang, D., Yang, Z.: Modular checking for buffer overflows in the large. In: ICSE ’06: Proceedings of the 28th international conference on Software engineering. pp. 232–241. ACM, New York (2006)

  16. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 and 583 (1969)

    Google Scholar 

  17. Hoare, C.A.R.: Procedures and Parameters: an Axiomatic Approach. In: Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188, pp. 102–116. Springer Berlin (1971)

  18. Hoare C.A.R.: Proof of correctness of data representations. Acta Inform. 1(4), 271–281 (1972)

    Article  MATH  Google Scholar 

  19. Hubert, T., Marché, C.: Separation analysis for deductive verification. In: Heap Analysis and Verification (HAV’07). pp. 81–93. Braga (2007)

  20. Joshi R., Leino K.R.M.: A semantic approach to secure information flow. Sci Comput Program 37(1–3), 113–138 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  21. Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML Reference Manual (draft) (2009)

  22. Marché, C., Paulin-Mohring, C.: Reasoning about Java programs with aliasing and frame conditions. In: 18th International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 3603, pp. 179–194 (2005)

  23. Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) European Symposium on Programming (ESOP’05). Lecture Notes in Computer Science, vol. 3444, pp. 5–20. Springer, Berlin (2005)

  24. Meyer B.: Object-oriented Software Construction. Prentice Hall, New Jersey (1997)

    MATH  Google Scholar 

  25. Moy, Y.: Union and cast in deductive verification. In: Proceedings of the C/C++ Verification Workshop. vol. Technical Report ICIS-R07015, pp. 1–16. Radboud University Nijmegen (2007)

  26. Moy, Y.: Automatic Modular Static Safety Checking for C Programs. Ph.D. thesis, Université Paris Sud (2009)

  27. Moy, Y., Marché, C.: Inferring local (non-)aliasing and strings for memory safety. In: Heap Analysis and Verification (HAV’07). pp. 35–51. Braga (2007)

  28. Praxis High Integrity Systems: SPARK95 - The SPADE Ada 95 Kernel (Including RavenSPARK), 4.8 edn. http://www.altran-praxis.com/downloads/SPARK/technicalReferences/SPARK95RavenSPARK.pdf (2008)

  29. Formalization in Coq of the equivalence between the two formulations of functional dependencies. http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:functional-dependencies

  30. Randimbivololona, F., Souyris, J., Baudin, P., Pacalet, A., Raguideau, J., Schoen, D.: Applying formal proof techniques to avionics software: a pragmatic approach. In: World Congress on Formal Methods. Lecture Notes in Computer Science, vol. 1709, pp. 1798–1815. Springer, Berlin (1999)

  31. Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS. pp. 55–74. IEEE Computer Society, California (2002)

  32. RTCA and EUROCAE: DO-178B - Software Considerations in Airborne Systems and Equipment Certification (1992)

  33. WG14: ISO C Standard 1999. Tech. rep., ISO. http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf, ISO/IEC 9899: 1999 draft (1999)

  34. Why home page. http://why.lri.fr/

Download references

Author information

Authors and Affiliations

  1. CEA, LIST, Laboratoire de Sûreté des Logiciels, Boîte courrier 94, 91191, Gif-sur-Yvette Cedex, France

    Pascal Cuoq, Benjamin Monate & Virgile Prevosto

  2. INRIA Sophia Antipolis, 2004 route des Lucioles, BP93, 06902, Sophia Antipolis Cedex, France

    Anne Pacalet

Authors
  1. Pascal Cuoq
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benjamin Monate
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anne Pacalet
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Virgile Prevosto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pascal Cuoq.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Cuoq, P., Monate, B., Pacalet, A. et al. Functional dependencies of C functions via weakest pre-conditions. Int J Softw Tools Technol Transfer 13, 405–417 (2011). https://doi.org/10.1007/s10009-011-0192-z

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-011-0192-z

Keywords

Search

Navigation