ISSN:
1573-7640
Keywords:
Concurrency
;
verification
;
computer-aided reasoning
;
semantics
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract This paper describes the use of an automated reasoning tool, the Nuprl system, to formalize Milner's Calculus of Communicating Systems (CCS). The goals of this work are two-fold: the first is to investigate the feasibility of using systems like Nuprl to handle the formal detail arising from reasoning about concurrency, while the second is to develop a framework in which various formalisms for reasoning about concurrency may be presented in an automated fashion. To these ends, an implementation in Nuprl of a formal theory of concurrency is described, an implementation of CCS in this mechanized semantic theory presented, and two means of analyzing CCS terms are investigated.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01383954
