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

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

doi:10.1145/2025113.2025182

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

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

Original language	English
Title of host publication	ESEC/FSE '11 Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering
Publisher	ACM
Pages	428-431
Number of pages	4
ISBN (Print)	978-1-4503-0443-6
DOIs	https://doi.org/10.1145/2025113.2025182
Publication status	Published - 5 Sept 2011
Event	19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC/FSE) - Szeged, Hungary Duration: 5 Sept 2011 → 9 Sept 2011

Conference

Conference	19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC/FSE)
Country/Territory	Hungary
City	Szeged
Period	5/09/11 → 9/09/11

Access to Document

10.1145/2025113.2025182

http://dl.acm.org/citation.cfm?id=2025113.2025182

Cite this

@inproceedings{bd51816b860d4f3fb727016421e2f28d,

title = "jStar-eclipse: an IDE for automated verification of Java programs",

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.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.",

author = "Daiva Naudziuniene and Matko Botincan and Dino Distefano and Mike Dodds and Radu Grigore and Parkinson, {Matthew J.}",

year = "2011",

month = sep,

day = "5",

doi = "10.1145/2025113.2025182",

language = "English",

isbn = "978-1-4503-0443-6",

pages = "428--431",

booktitle = "ESEC/FSE '11 Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering",

publisher = "ACM",

address = "United States",

note = "19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC/FSE) ; Conference date: 05-09-2011 Through 09-09-2011",

}

Naudziuniene, D, Botincan, M, Distefano, D, Dodds, M, Grigore, R & Parkinson, MJ 2011, jStar-eclipse: an IDE for automated verification of Java programs. in ESEC/FSE '11 Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering. ACM, pp. 428-431, 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC/FSE), Szeged, Hungary, 5/09/11. https://doi.org/10.1145/2025113.2025182

jStar-eclipse: an IDE for automated verification of Java programs. / Naudziuniene, Daiva; Botincan, Matko; Distefano, Dino et al.
ESEC/FSE '11 Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering. ACM, 2011. p. 428-431.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Naudziuniene, Daiva

AU - Botincan, Matko

AU - Distefano, Dino

AU - Dodds, Mike

AU - Grigore, Radu

AU - Parkinson, Matthew J.

PY - 2011/9/5

Y1 - 2011/9/5

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

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

U2 - 10.1145/2025113.2025182

DO - 10.1145/2025113.2025182

M3 - Conference contribution

SN - 978-1-4503-0443-6

SP - 428

EP - 431

BT - ESEC/FSE '11 Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering

PB - ACM

T2 - 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC/FSE)

Y2 - 5 September 2011 through 9 September 2011

ER -