coreStar: the core of jStar
Published in 1st International Workshop on Intermediate Verification Languages (Boogie 2011), 2011
Abstract: Separation logic is a promising approach to program verification. However, currently there is no shared infrastructure for building verification tools. This increases the time to build and experiment with new ideas. In this paper, we outline coreStar, the verification framework underlying jStar. Our aim is to provide basic support for developing separation logic tools. This paper shows how a language can be encoded into coreStar, and gives details of how coreStar works to enable extensions.
Paper: PDF