kirancodes.me
To Proof Maintenance & Beyond!
FSE 2011

jStar-eclipse: an IDE for automated verification of Java programs

Daiva Naudziuniene, Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Matthew J. Parkinson

PDFDOI 10.1145/2025113.2025182dblp

Abstract

jStar is a tool for automatically verifying Java programs. It uses separation logic to support abstract reasoning about object specifications. jStar can verify a number of challenging design patterns, including Subject/Observer, Visitor, Factory and Pooling. However, to use jStar one has to deal with a family of command-line tools that expect specifications in separate files and diagnose the errors by inspecting the text output from these tools.

BibTeX
@inproceedings{Naudziuniene-al:FSE11,
  author    = {Daiva Naudziuniene and
               Matko Botincan and
               Dino Distefano and
               Mike Dodds and
               Radu Grigore and
               Matthew J. Parkinson},
  title     = {{jStar-eclipse:} an {IDE} for automated verification of Java programs},
  booktitle = {FSE},
  pages     = {428--431},
  publisher = {{ACM}},
  year      = {2011},
}

Related papers