期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2009
卷号：8
页码：26-40
DOI：10.4204/EPTCS.8.3
出版社：Open Publishing Association
摘要：Separation Logic is a non-classical logic used to verify pointer-intensive code. In this paper, however, we show that Separation Logic, along with its natural extensions, can also be used as a specification language for concurrent-system design. To do so, we express the behavior of three very different concurrent systems: a Subway, a Stopwatch, and a 2x2 Switch. The Subway is originally implemented in LUSTRE, the Stopwatch in Esterel, and the 2x2 Switch in Bluespec.
