×

A Coq library for verification of concurrent programs. (English) Zbl 1278.68152

Schürmann, C. (ed.), Proceedings of the fourth international workshop on logical frameworks and meta-languages (LFM 2004), Cork, UK, July 5, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 199, 17-32 (2008).
Summary: Thanks to recent advances, modern proof assistants now enable verification of realistic sequential programs. However, regarding the concurrency paradigm, previous work essentially focused on formalization of abstract systems, such as pure concurrent calculi, which are too minimal to be realistic. In this paper, we propose a library that enables verification of realistic concurrent programs in the Coq proof assistant. Our approach is based on an extension of the \(\pi\)-calculus whose encoding enables such programs to be modeled conveniently. This encoding is coupled with a specification language akin to spatial logics, including in particular a notion of fairness, which is important to write satisfactory specifications for realistic concurrent programs. In order to facilitate formal proof, we propose a collection of lemmas that can be reused in the context of different verifications. Among these lemmas, the most effective for simplifying the proof task take advantage of confluence properties. In order to evaluate feasibility of verification of concurrent programs using this library, we perform verification for a non-trivial application.
For the entire collection see [Zbl 1276.68030].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Coq; Why3; Pict; HOL; Isabelle/HOL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, Martín, and Cédric Fournet, Mobile values, new names, and secure communication28th ACM Symposium on Principles of Programming Languages (POPL 2001); Abadi, Martín, and Cédric Fournet, Mobile values, new names, and secure communication28th ACM Symposium on Principles of Programming Languages (POPL 2001) · Zbl 1323.68398
[2] Affeldt, Reynald; Kobayashi, Naoki, Formalization and verification of a mail server in Coq, (International Symposium on Software Security. International Symposium on Software Security, Lecture Notes in Computer Science, volume 2609 (Feb. 2003), Springer-Verlag), 217-233 · Zbl 1033.68502
[3] Affeldt, Reynald; Kobayashi, Naoki, A Coq Library for Verification of Concurrent Programs, Coq scripts · Zbl 1278.68152
[4] Affeldt, Reynald; Kobayashi, Naoki, Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes, 11th International Workshop on Expressiveness in Concurrency. 11th International Workshop on Expressiveness in Concurrency, (EXPRESS 2004). 11th International Workshop on Expressiveness in Concurrency. 11th International Workshop on Expressiveness in Concurrency, (EXPRESS 2004), Electronic Notes in Theoretical Computer Science, 128, 2, 151-168 (2005), Elsevier · Zbl 1272.68217
[5] Black, Paul E., “Axiomatic Semantics Verification of a Secure Web Server,” Ph.D. thesis, Department of Computer Science, Brigham Young University, 1998; Black, Paul E., “Axiomatic Semantics Verification of a Secure Web Server,” Ph.D. thesis, Department of Computer Science, Brigham Young University, 1998
[6] Boulton, Richard, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel, Experience with embedding hardware description languages in HOLIFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience; Boulton, Richard, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel, Experience with embedding hardware description languages in HOLIFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience
[7] Cardelli, Luca, and Andrew D. Gordon, Anytime, anywhere: modal logics for mobile ambients27th ACM Symposium on Principles of Programming Languages (POPL 2000); Cardelli, Luca, and Andrew D. Gordon, Anytime, anywhere: modal logics for mobile ambients27th ACM Symposium on Principles of Programming Languages (POPL 2000) · Zbl 1323.68405
[8] Cervesato, Iliano, Frank Pfenning, David Walker, and Kevin Watkins, A concurrent logical framework II: Examples and applications; Cervesato, Iliano, Frank Pfenning, David Walker, and Kevin Watkins, A concurrent logical framework II: Examples and applications · Zbl 1100.68548
[9] Coupet-Grimal, Solange, An axiomatization of linear temporal logic in the calculus of inductive constructions, Journal of Logic and Computation, 13, 6, 801-813 (2003) · Zbl 1093.68024
[10] Coupet-Grimal, Solange; Nouvet, Catherine, Formal verification of an incremental garbage collector, Journal of Logic and Computation, 13, 6, 815-833 (2003) · Zbl 1074.68548
[11] Dam, Mads, Proof Systems for the pi-calculus Logics, Logic for Concurrency and Synchronisation. Logic for Concurrency and Synchronisation, Trends in Logic, Logica Library (2003), Kluwer · Zbl 1038.03034
[12] Despeyroux, Joëlle; Felty, Amy; Hirschowitz, André, Higher-Order Abstract Syntax in Coq, (2nd International Conference on Typed Lambda Calculi and Applications. 2nd International Conference on Typed Lambda Calculi and Applications, (TLCA 1995). 2nd International Conference on Typed Lambda Calculi and Applications. 2nd International Conference on Typed Lambda Calculi and Applications, (TLCA 1995), Lecture Notes in Computer Science, volume 905 (Apr. 1995), Springer-Verlag), 124-138 · Zbl 1063.68650
[13] Despeyroux, Joëlle, A higher-order specification of the \(π\)-calculus, (IFIP Conference on Theoretical Computer Science 2000. IFIP Conference on Theoretical Computer Science 2000, Lecture Notes in Computer Science, volume 1872 (Aug. 2000), Springer-Verlag), 425-439 · Zbl 0998.68538
[14] Filliâtre, Jean-Christophe, Why: a multi-language multi-prover verification tool; Filliâtre, Jean-Christophe, Why: a multi-language multi-prover verification tool
[15] Gay, Simon J., A framework for the formalisation of pi calculus type systems in Isabelle/HOL, (Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, (TPHOLs 2001). Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, (TPHOLs 2001), Lecture Notes in Computer Science, volume 2152 (Sep. 2001), Springer-Verlag), 217-232 · Zbl 1005.68531
[16] Heyd, Barbara; Crégut, Pierre, A modular coding of UNITY in Coq, (Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, (TPHOLs 1996). Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, (TPHOLs 1996), Lecture Notes in Computer Science, volume 1125 (Aug. 1996), Springer-Verlag), 251-266
[17] Hirschkoff, Daniel, “Mise en œuvre de preuves de bisimulation,” Ph.D. thesis, École Nationale des Ponts et Chaussées, 1999; Hirschkoff, Daniel, “Mise en œuvre de preuves de bisimulation,” Ph.D. thesis, École Nationale des Ponts et Chaussées, 1999
[18] Honsell, Furio; Miculan, Marino; Scagnetto, Ivan, \(π\)-calculus in (co)inductive type theory, Theoretical Computer Science, 253, 2, 239-285 (Feb. 2001)
[19] Kobayashi, Naoki, A type system for lock-free processes, Information and Computation, 177, 2, 122-159 (Sep. 2002)
[20] Kobayashi, Naoki, Type systems for concurrent programs, (UNU/IIST 10th Anniversary Colloquium. UNU/IIST 10th Anniversary Colloquium, March 2002, Lisbon, Portugal (2002), Springer-Verlag), Tutorial · Zbl 1274.68076
[21] Kobayashi, Naoki, Benjamin C. Pierce, and David N. Turner, Linearity and the Pi-Calculus23rd ACM Symposium on Principles of Programming Languages (POPL 1996); Kobayashi, Naoki, Benjamin C. Pierce, and David N. Turner, Linearity and the Pi-Calculus23rd ACM Symposium on Principles of Programming Languages (POPL 1996)
[22] Manolios, Panagiotis, “Mechanical Verification of Reactive Systems,” Ph.D. thesis, The University of Texas at Austin, Department of Computer Sciences, Austin, TX, 2001; Manolios, Panagiotis, “Mechanical Verification of Reactive Systems,” Ph.D. thesis, The University of Texas at Austin, Department of Computer Sciences, Austin, TX, 2001 · Zbl 1003.68150
[23] Melham, Thomas F., A Mechanized Theory of the \(π\)-calculus in HOL, Nordic Journal of Computing, 1, 1, 50-76 (1995)
[24] Milner, Robin; Parrow, Joachim; Walker, David, A calculus of mobile processes, parts I and II, Information and Computation, 100, 1, 1-77 (1992) · Zbl 0752.68037
[25] Paulson, Lawrence C., Mechanizing a theory of program composition for UNITY, ACM Transactions on Programming Languages and Systems, 23, 5, 626-656 (2001)
[26] Pierce, Benjamin C.; Turner, David N., Pict: A programming language based on the pi-calculus, Proof, Language and Interaction: Essays in Honour of Robin Milner (2000), MIT Press
[27] Pierce, Benjamin C., and Jérôme Vouillon, Specifying a file synchronizer; Pierce, Benjamin C., and Jérôme Vouillon, Specifying a file synchronizer
[28] Röckl, Christine; Hirschkoff, Daniel; Berghofer, Stefan, Higher-order abstract syntax with induction in Isabelle/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts, (Foundations of Software Science and Computation Structures. Foundations of Software Science and Computation Structures, (FOSSACS 2001). Foundations of Software Science and Computation Structures. Foundations of Software Science and Computation Structures, (FOSSACS 2001), Lecture Notes in Computer Science, number 2030 (Apr. 2001), Springer-Verlag) · Zbl 0978.68045
[29] Scagnetto, Ivan; Miculan, Marino, Ambient calculus and its logic in the calculus of inductive constructions, 3rd International Workshop on Logical Frameworks and Meta-Languages. 3rd International Workshop on Logical Frameworks and Meta-Languages, (LFM 2002). 3rd International Workshop on Logical Frameworks and Meta-Languages. 3rd International Workshop on Logical Frameworks and Meta-Languages, (LFM 2002), Electronic Notes in Theoretical Computer Science, 70, 2 (2002), Elsevier · Zbl 1270.03052
[30] The Coq Development Team, “The Coq Proof Assistant Reference Manual,” INRIA, 2004; The Coq Development Team, “The Coq Proof Assistant Reference Manual,” INRIA, 2004
[31] Watkins, Kevin, Iliano Cervesato, Frank Pfenning, and David Walker, A concurrent logical framework I: Judgments and properties; Watkins, Kevin, Iliano Cervesato, Frank Pfenning, and David Walker, A concurrent logical framework I: Judgments and properties · Zbl 1100.68548
[32] Yu, Shen-Wei, “Formal Verification of Concurrent Programs Based on Type Theory,” Ph.D. thesis, Department of Computer Science, University of Durham, 1998; Yu, Shen-Wei, “Formal Verification of Concurrent Programs Based on Type Theory,” Ph.D. thesis, Department of Computer Science, University of Durham, 1998
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.