Verifying C Programs
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.
KeywordsProof Obligation Verification Condition Safety Behaviour Verification Tool Array Position
- 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.Filliâtre, J.-C.: Program verification using coq—introduction to the why tool. Lecture Notes TYPES Summer School (2005) Google Scholar
- 4.Filliâtre, J.-C.: Queens on a chessboard: An exercise in program verification (2007).http://why.lri.fr/queens/
- 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.Moy, Y., Marché, C., Jessie Plugin Tutorial. LRI (February 2010). Beryllium Version Google Scholar