Expressing the Behavior of Three Very Different Concurrent Systems by Using Natural Extensions of Separation Logic

Edgar G. Daylight
(Institute of Logic, Language, and Computation, University of Amsterdam)
Sandeep K. Shukla
(Department of Electrical and Computer Engineering, Virginia Tech)
Davide Sergio
(Institute of Logic, Language, and Computation, University of Amsterdam)

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.

In Sibylle Fröschle and Daniele Gorla: Proceedings 16th International Workshop on Expressiveness in Concurrency (EXPRESS 2009), Bologna, Italy, 5th September 2009, Electronic Proceedings in Theoretical Computer Science 8, pp. 26–40.
Published: 17th November 2009.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: