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

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

arxiv: 0911.2034 · v1 · submitted 2009-11-11 · 💻 cs.LO · cs.SE

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

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

classification 💻 cs.LO cs.SE

keywords logicseparationbehaviorconcurrentdifferentextensionsnaturalstopwatch

0 comments

read the original abstract

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.

This paper has not been read by Pith yet.

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

discussion (0)