License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2023.40
URN: urn:nbn:de:0030-drops-182330
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18233/
Mota, João ;
Giunti, Marco ;
Ravara, António
On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper)
Abstract
Typestates are a notion of behavioral types that describe protocols for stateful objects, specifying the available methods for each state. Ensuring methods are called in the correct order (protocol compliance), and that, if and when the program terminates, all objects are in the final state (protocol completion) is crucial to write better and safer programs. Objects of this kind are commonly shared among different clients or stored in collections, which may also be shared. However, statically checking protocol compliance and completion when objects are shared is challenging. To evaluate the support given by state of the art verification tools in checking the correct use of shared objects with protocol, we present a survey on four tools for Java: VeriFast, VerCors, Plural, and KeY. We describe the implementation of a file reader, linked-list, and iterator, check for each tool its ability to statically guarantee protocol compliance and completion, even when objects are shared in collections, and evaluate the programmer’s effort in making the code acceptable to these tools. With this study, we motivate the need for lightweight methods to verify the presented kinds of programs.
BibTeX - Entry
@InProceedings{mota_et_al:LIPIcs.ECOOP.2023.40,
author = {Mota, Jo\~{a}o and Giunti, Marco and Ravara, Ant\'{o}nio},
title = {{On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage}},
booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)},
pages = {40:1--40:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-281-5},
ISSN = {1868-8969},
year = {2023},
volume = {263},
editor = {Ali, Karim and Salvaneschi, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18233},
URN = {urn:nbn:de:0030-drops-182330},
doi = {10.4230/LIPIcs.ECOOP.2023.40},
annote = {Keywords: Java, Typestates, VeriFast, VerCors, Plural, KeY}
}
