×

coreStar

swMATH ID: 18520
Software Authors: M Botincan, D Distefano, M Dodds, et. al.
Description: coreStar: The Core of jStar. 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.
Homepage: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.231.9779&rep=rep1&type=pdf#page=69
Related Software: VeriFast; Cyclist; Smallfoot; SLAyer; Predator; Slide; Infer; THOR; HIP; Dafny; Viper; Grasshopper; VerCors; Boogie; Chalice; Frama-C; Spec#; JML; Why3; KRAKATOA
Referenced in: 3 Publications

Referenced in 0 Serials

Referencing Publications by Year