Verification of Program Properties Using Different Theorem Provers: A Case Study

  • J. Santiago Jorge
  • Victor M. Gulias
  • Laura M. Castro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4739)


This paper explores the use of theorem provers to certify particular properties of software. Two different proof assistants are used to illustrate the method: Coq and Pvs. By comparing two theorem provers, conclusions about their suitability can be stated. The selected scenario is part of a real-world application: a distributed Video-on-Demand server. The development consists on two steps: first, the definition of a model of the algorithm to be studied in the proof assistants; second, the development and proving of the theorems.


Media Object Proof Assistant Interval Sequence Program Property Software Development Life Cycle 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Computing Surveys 28, 626–643 (1996)CrossRefGoogle Scholar
  2. 2.
    Peled, D.A.: Software Reliability Methods. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  3. 3.
    Jorge, J.S.: Estudio de la verificación de propiedades de programas funcionales: de las pruebas manuales al uso de asistentes de pruebas. PhD thesis, University of A Coruña, Spain (2004)Google Scholar
  4. 4.
    Jorge, J.S., Gulías, V.M., Cabrero, D.: Certifying Properties of Programs using Theorem Provers. In: Verification, Validation and Testing in Software Engineering, pp. 220–267. Idea Group Publishing, USA (2007)Google Scholar
  5. 5.
    Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  6. 6.
    Owre, S., Shankar, N., Rushby, J.M.: The PVS Specification Language. Computer Science Laboratory, SRI International (1995)Google Scholar
  7. 7.
    Gulías, V.M., Barreiro, M., Freire, J.L.: VODKA: Developing a video-on-demand server using distributed functional programming. Journal of Functional Programming 15, 403–430 (2005)zbMATHCrossRefGoogle Scholar
  8. 8.
    Armstrong, J., Virding, R., Wikström, C., Williams, M.: oncurrent Programming in Erlang, 2nd edn. Prentice Hall, Englewood Cliffs (1996)Google Scholar
  9. 9.
    Bird, R., Wadler, P.: Introduction to Functional Programming. Prentice Hall, Englewood Cliffs (1988)Google Scholar
  10. 10.
    Hudak, P.: Conception, evolution, and application of functional programming languages. ACM Computing Surveys 21, 359–411 (1989)CrossRefGoogle Scholar
  11. 11.
    Giménez, E.: A tutorial on recursive types in Coq. Technical report, INRIA, for Coq V6.2 (1998)Google Scholar
  12. 12.
    Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq proof assistant: A tutorial, v8.0. Technical report, INRIA (2004)Google Scholar
  13. 13.
    Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: WIFT 1995 Workshop on Industrial-Strength Formal Specification Techniques (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • J. Santiago Jorge
    • 1
  • Victor M. Gulias
    • 1
  • Laura M. Castro
    • 1
  1. 1.MADS group, Department of Computer Science, Universidade da Coruña, Campus de Elviña, s/n, 15071 A CoruñaSpain

Personalised recommendations