jStar-eclipse
Daiva Naudžiūnienė, Matko Botinčan, Dino Distefano, Mike Dodds, Radu Gheorghe Grigore, Matthew Parkinson · 2011
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.