TY - JOUR

T1 - Formalizing process algebraic verifications in the calculus of constructions

AU - Bezem, M.A.

AU - Bol, R.N.

AU - Groote, J.F.

PY - 1997

Y1 - 1997

N2 - 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 a ugmented 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.

AB - 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 a ugmented 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.

U2 - 10.1007/BF01212523

DO - 10.1007/BF01212523

M3 - Article

SN - 0934-5043

VL - 9

SP - 1

EP - 48

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

ER -