





















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.
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。