Advertisement

Verifying C Programs

  • José Bacelar Almeida
  • Maria João Frade
  • Jorge Sousa Pinto
  • Simão Melo de Sousa
Part of the Undergraduate Topics in Computer Science book series (UTICS)

Abstract

In this chapter we study a verification tool, called Frama-C, for ACSL-annotated C programs. In fact Frama-C is much more than a verification tool: it is a general, plug-in-based program analysis tool, designed to be used in practice in industrial projects. The program verification functionality of Frama-C used in the present chapter is provided by the Jessie plug-in. Jessie in turn relies on the use of a multi-prover VCGen tool that can export verification conditions to many different proof tools, including for instance the Simplify and Z3 automatic provers, and proof assistants like Coq.

Our approach in the present chapter is to start from an algorithm for which only an informal specification is given. We annotate the C code of this function as we go along, starting with the minimal annotations required for verification of safety, followed later by other functional properties.

Keywords

Proof Obligation Verification Condition Safety Behaviour Verification Tool Array Position 
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.

References

  1. 1.
    Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, vol. 3362, pp. 49–69. Springer, Berlin (2004) CrossRefGoogle Scholar
  2. 2.
    Barnett, M., Chang, B.-Y.E., 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. Lecture Notes in Computer Science, vol. 4111, pp. 364–387. Springer, Berlin (2005) Google Scholar
  3. 3.
    Filliâtre, J.-C.: Program verification using coq—introduction to the why tool. Lecture Notes TYPES Summer School (2005) Google Scholar
  4. 4.
    Filliâtre, J.-C.: Queens on a chessboard: An exercise in program verification (2007).http://why.lri.fr/queens/
  5. 5.
    Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV. Lecture Notes in Computer Science, vol. 4590, pp. 173–177. Springer, Berlin (2007) Google Scholar
  6. 6.
    Moy, Y., Marché, C., Jessie Plugin Tutorial. LRI (February 2010). Beryllium Version Google Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  • José Bacelar Almeida
    • 1
  • Maria João Frade
    • 2
  • Jorge Sousa Pinto
    • 1
  • Simão Melo de Sousa
    • 2
  1. 1.Depto. InformáticaUniversidade do MinhoBragaPortugal
  2. 2.Depto. InformáticaUniversidade Beira InteriorCovilhãPortugal

Personalised recommendations