Formalizing process algebraic verifications in the calculus of constructions
- 1 January 1997
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 9 (1) , 1-48
- https://doi.org/10.1007/bf01212523
Abstract
This paper reports on the first steps towards the formal verification of correctness proofs of real-life protocols in process algebra. We show that such proofs can be verified, and partly constructed, by a general purpose proof checker. The process algebra we use isμCRL, ACPτaugmented with data, which is expressive enough for the specification of real-life protocols. The proof checker we use is Coq, which is based on the Calculus of Constructions, an extension of simply typed lambda calculus. The focus is on the translation of the proof theory ofμCRL andμCRL-specifications to Coq. As a case study, we verified the Alternating Bit Protocol.Keywords
This publication has 22 references indexed in Scilit:
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Nature ,2005
- A bounded retransmission protocol for large data packetsPublished by Springer Nature ,1996
- Wait-free linearization with a mechanical proofDistributed Computing, 1995
- The Syntax and Semantics of μCRLPublished by Springer Nature ,1995
- Wait-free linearization with an assertional proofDistributed Computing, 1994
- Proof Theory for µCRL: A Language for Processes with Data.Published by Springer Nature ,1994
- A Correctness Proof of a One-bit Sliding Window Protocol in CRLThe Computer Journal, 1994
- Type theory and concurrencyInternational Journal of Parallel Programming, 1988
- Proving Liveness Properties of Concurrent ProgramsACM Transactions on Programming Languages and Systems, 1982
- A note on reliable full-duplex transmission over half-duplex linksCommunications of the ACM, 1969