Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 542909

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


Naudziuniene, Daiva; Botinčan, Matko; Distefano, Dino; Dodds, Mike; Grigore, Radu; Parkinson, Matthew J.
jStar-eclipse: an IDE for automated verification of Java programs // Proceedings of the 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2011) / Gymothy, Tibor ; Zeller, Andreas (ur.).
New York: ACM, 2011. str. 428-431 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


CROSBI ID: 542909 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

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 : 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.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


Projekti:
037-0362980-2774 - Distribuirani algoritmi za pronalaženje optimalnih putova u grafovima (Manger, Robert, MZOS ) ( POIROT)

Ustanove:
Prirodoslovno-matematički fakultet, Matematički odjel, Zagreb

Profili:

Avatar Url Matko Botinčan (autor)


Citiraj ovu publikaciju:

Naudziuniene, Daiva; Botinčan, Matko; Distefano, Dino; Dodds, Mike; Grigore, Radu; Parkinson, Matthew J.
jStar-eclipse: an IDE for automated verification of Java programs // Proceedings of the 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2011) / Gymothy, Tibor ; Zeller, Andreas (ur.).
New York: ACM, 2011. str. 428-431 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
Naudziuniene, D., Botinčan, M., Distefano, D., Dodds, M., Grigore, R. & Parkinson, M. (2011) jStar-eclipse: an IDE for automated verification of Java programs. U: Gymothy, T. & Zeller, A. (ur.)Proceedings of the 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2011).
@article{article, author = {Naudziuniene, Daiva and Botin\v{c}an, Matko and Distefano, Dino and Dodds, Mike and Grigore, Radu and Parkinson, Matthew J.}, year = {2011}, pages = {428-431}, keywords = {automated verification, separation logic, Java, Eclipse}, isbn = {978-1-4503-0443-6}, title = {jStar-eclipse: an IDE for automated verification of Java programs}, keyword = {automated verification, separation logic, Java, Eclipse}, publisher = {ACM}, publisherplace = {Szeged, Ma\djarska} }
@article{article, author = {Naudziuniene, Daiva and Botin\v{c}an, Matko and Distefano, Dino and Dodds, Mike and Grigore, Radu and Parkinson, Matthew J.}, year = {2011}, pages = {428-431}, keywords = {automated verification, separation logic, Java, Eclipse}, isbn = {978-1-4503-0443-6}, title = {jStar-eclipse: an IDE for automated verification of Java programs}, keyword = {automated verification, separation logic, Java, Eclipse}, publisher = {ACM}, publisherplace = {Szeged, Ma\djarska} }




Contrast
Increase Font
Decrease Font
Dyslexic Font