Journal article icon

Journal article

Type inference and strong static type checking for Promela

Abstract:

The Spin model checker and its specification language Promela have been used extensively in industry and academia to check the logical properties of distributed algorithms and protocols. Model checking with Spin involves reasoning about a system via an abstract Promela specification, thus the technique depends critically on the soundness of this specification. Promela includes a rich set of data types including first-class channels, but the language syntax restricts the declaration of chan...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Publisher's version

Actions


Access Document


Files:
Publisher copy:
10.1016/j.scico.2010.05.010

Authors


More by this author
Institution:
University of Oxford
Department:
Computing Laboratory
Role:
Author
Publisher:
Elsevier B.V. Publisher's website
Journal:
Science of Computer Programming Journal website
Volume:
75
Issue:
11
Pages:
1165-1191
Publication date:
2010-11-05
DOI:
ISSN:
0167-6423
URN:
uuid:1da1baaf-85d8-4d30-8f57-b3bc99081969
Local pid:
ora:9655

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP