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

Edgar G. Daylight, Sandeep K. Shukla, Davide Sergio

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…