Skip to main content
SpringerLink
Log in

Formal verification of concurrent programs in Lp and in Coq: A comparative analysis

  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1275))

Included in the following conference series:

Abstract

This paper describes the formal verification of parallel programs using a rewrite and induction based theorem prover like LP and a higher order theorem prover based on the Calculus of Inductive Construction, namely Coq. The chosen specification environment is UNITY, a subset of temporal logic for specifying and verifying concurrent programs. By means of an example, a lift-control program, we describe the embedding Of UNITY and we show how to verify mechanically program properties using the two provers. Then we summarize a comparison between the theorem proving environments, based on our practical experience with both systems for the verification of UNITY programs.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Andersen. A theorem Proyer for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, 1992.

    Google Scholar 

  2. F. Andersen, K.D. Petersen, and J.S. Pettersson. Program verification using HOL-Unity. In J.J. Joyce and C.H. Seger, editors, Proceedings sixth International Workshop on Higher Order Logic theorem proving and its applications, volume 780 of Lecture Notes in Computer Science, pages 1–15, Vancouver, Canada, August 1993. Springer-Verlag.

    Google Scholar 

  3. D Bolignano. Towards a Mechanization of Cryptographic Protocol Verification. In Conference On Computer-Aided Verification, Haifa, Israël, Jun 1997. Springer-Verlag.

    Google Scholar 

  4. N. Brown and D. Merl A proof environment for concurrent programs. In In Proceedings FME'93 Symposium, volume 670 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

    Google Scholar 

  5. K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988. ISBN 0-201-05866-9.

    Google Scholar 

  6. B. Chetali. Vérification Formelle des Systèmes Parallèles décrits en UNITY á l'aide d'un outil de Démonstration Automatique. PhD thesis, Université Henri Poincaré, Nancy l., May 1996.

    Google Scholar 

  7. B. Chetali and P. Lescanne. An exercise in LP: The proof of the non restoring division circuit. In U. Martin and J.M. Wing, editors, Proceedings First International Workshop on Larch, volume 780 of Workshops in Computing, pages 55–68, Dedbam, Boston, August 1992. Springer-Verlag.

    Google Scholar 

  8. B. Chetali and P. Lescarme. Formal verification of a protocol for communications over faulty channels. In Proc., of the 8th International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols (FORTE'95), Montréal, Quebec, Canada, October 1995. IFIP.

    Google Scholar 

  9. Projet Coq. The coq proof assistant (version 6.1). Reference Manual, 1996

    Google Scholar 

  10. S Coupet-Grimai and L Jakubiec. Coq and Hardward Verification: A Case Study. In J von Wright, J Grundy, and J Harrison, editors, Theorem Proving In Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 125–139, Turku, Finland, August 1996. Springer-Verlag.

    Google Scholar 

  11. P Crégut. Omega: A solver of quantifier-free problems in presburger arithmetic. Supplied in the contrib directory of Coq V6.1, 1996.

    Google Scholar 

  12. E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, 1989.

    Google Scholar 

  13. D. Doligez and G. Gonthier. Portable, unobtrusive garbage collection for multiprocessor systems. In POPL'94. ACM, 1994.

    Google Scholar 

  14. S. V. Garland and J. V. Guttag. A guide to LP, the Larch prover. Technical Report 82, Digital Systems Research Center, 130 Lytton Ave., Palo Alto, CA 94301, USA., 1991.

    Google Scholar 

  15. E. Giménez. A Calculus of Infinite Constructions and its application to the verification of communicating systems. PhD thesis, Ecole Normale Supérieure de Lyon, 1996.

    Google Scholar 

  16. D. M. Goldschlag. Mechanically verifying concurrent programs with the Boyer-Moore Prover. IEEE Transactions on Software Engineering, 16(9):1005–1022, September 1990.

    Google Scholar 

  17. J. V. Guttag, J.J. Horning, S.J Garland, K.D. Jones, A. Modet, and J. M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.

    Google Scholar 

  18. B Heyd and P. Crégut. A modular coding of Unity in Coq. In J von Wright, J Grundy, and J Harrison, editors, Theorem Proving in Higher Order Logic, volume 1125 of Lecture Notes in Computer Science, pages 251–266, Turku, Finland, August 1996. Springer-Verlag.

    Google Scholar 

  19. L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 3(2):125–143, 1977.

    Google Scholar 

  20. L. Lamport and S. Owicki. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, may 1994.

    Google Scholar 

  21. Victor Luchangco, Ekrem Séylemez, Stephen Garland, and Nancy Lynch. Verifying timing properties of concurrent algorithms. In FORTE'94: Seventh International Conference on Formal Description Techniques, Berne, Switzerland, October 4–7 1994. Chapman and Hall.

    Google Scholar 

  22. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer-Verlag, 1991.

    Google Scholar 

  23. N. Mellergaard and J. Staunstrup. Generating proof obligations for circuits. In Ursula Martin and Jeannette M. Wing, editors, First International Workshop on Larch, pages 185–199. Springer-Verlag, July 1992.

    Google Scholar 

  24. J. Misra. A logic for concurrent programming. unpublished manuscripts, 1994.

    Google Scholar 

  25. S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2), February 1995.

    Google Scholar 

  26. C Paulin-Mohring. Circuits as Streams in Coq: Verification of a Sequential Multiplier. Basic Research Actions “Types”, 1995.

    Google Scholar 

  27. I.S.W.B. Prasetya. Error in the UNITY Substitution Rule for Subscripted Operators(Short Communication). 6(4):466–470, 1994.

    Google Scholar 

  28. B. A. Sanders. Eliminating the substitution axiom from UNITY logic. Formal Aspects of Computing, 3:189–205, 1991.

    Google Scholar 

  29. B Werner. Une théorie des constructions inductives. PhD thesis, Université Paris 7, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN-CNRS and INRIA-Lorraine, University of Henri Poincaré,Nancy I, Campus Scientifique -B.P. 101, 54602, Villers-les-Nancy, France

    Boutheina Chetali & Barbara Heyd

Authors
  1. Boutheina Chetali
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Barbara Heyd
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Elsa L. Gunter Amy Felty

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chetali, B., Heyd, B. (1997). Formal verification of concurrent programs in Lp and in Coq: A comparative analysis. In: Gunter, E.L., Felty, A. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1997. Lecture Notes in Computer Science, vol 1275. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028386

Download citation

  • DOI: https://doi.org/10.1007/BFb0028386

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63379-2

  • Online ISBN: 978-3-540-69526-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation