jStar-eclipse: an IDE for automated verification of Java programs (CROSBI ID 579429)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Naudziuniene, Daiva ; Botinčan, Matko ; Distefano, Dino ; Dodds, Mike ; Grigore, Radu ; Parkinson, Matthew J.
engleski
jStar-eclipse: an IDE for automated verification of Java programs
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. In this paper we present a plug-in, called jStar-eclipse, allowing programmers to use jStar from within Eclipse IDE. Our plug-in allows writing method contracts in Java source files in form of Java annotations. It automatically translates Java annotations into jStar specifications and propagates errors reported by jStar back to Eclipse, pinpointing the errors to the locations in source files. This way the plug-in ensures an overall better user experience when working with jStar. Our end goal is to make automated verification based on separation logic accessible to a broader audience.
automated verification; separation logic; Java; Eclipse
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
428-431.
2011.
objavljeno
Podaci o matičnoj publikaciji
Gymothy, Tibor ; Zeller, Andreas
New York (NY): The Association for Computing Machinery (ACM)
978-1-4503-0443-6
Podaci o skupu
The 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2011)
predavanje
05.09.2011-09.09.2011
Szeged, Mađarska