@inproceedings{167a6f63d6e14078a702c1c1f3d94197,
title = "A compositional proof of a real-time mutual exclusion protocol",
abstract = "In this paper, we apply a compositional proof technique to an automatic verification of the correctness of Fischer{\textquoteright}s mutual exclusion protocol. It is demonstrated that the technique may avoid the stateexplosion problem. Our compositional technique has recently been implemented in a tool CMC5, which verifies the protocol for 50 processes within 172.3 seconds and using only 32MB main memory. In contrast all existing verification tools for timed systems will suffer from the stateexplosion problem, and no tool has to our knowledge succeeded in verifying the protocol for more than 11 processes.",
author = "Kristoffersen, \{K{\aa}re J.\} and Francois Laroussinie and Larsen, \{Kim G.\} and Paul Pettersson and Wang Yi",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 7th International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1997 ; Conference date: 14-04-1997 Through 18-04-1997",
year = "1997",
doi = "10.1007/bfb0030626",
language = "英语",
isbn = "9783540627814",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "565--579",
editor = "Michel Bidoit and Michel Bidoit and Max Dauchet and Max Dauchet",
booktitle = "TAPSOFT 1997",
address = "德国",
}