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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.8.3 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |