Naslov
JStar-eclipse: an IDE for automated verification of Java programs

Autori
Naudziuniene, Daiva ; Botinčan, Matko ; Distefano, Dino ; Dodds, Mike ; Grigore, Radu ; Parkinson, Matthew J.

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2011) / Gymothy, Tibor ; Zeller, Andreas - New York (NY) : The Association for Computing Machinery (ACM), 2011, 428-431

ISBN
978-1-4503-0443-6

Skup
The 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2011)

Mjesto i datum
Szeged, Mađarska, 05.09.2011. - 09.09.2011

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
automated verification; separation logic; Java; Eclipse

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA