On using VeriFast, VerCors, Plural, and KeY to check object usage
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.
Fri 21 JulDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | ECOOP 7: Verification and TestingResearch Papers at Amazon Auditorium (Gates G20) Chair(s): Wenxi Wang University of Texas at Austin | ||
10:30 15mTalk | On using VeriFast, VerCors, Plural, and KeY to check object usage Research Papers João Mota NOVA School of Science and Technology, António Ravara NOVA LINCS & FCT, NOVA University of Lisbon, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa DOI | ||
10:45 15mTalk | Exact Separation Logic Research Papers Petar Maksimović Imperial College London, UK, Caroline Cronjäger Ruhr-Universität Bochum, Andreas Lööw Imperial College London, Julian Sutherland Imperial College London, Philippa Gardner Imperial College London DOI Pre-print | ||
11:00 15mTalk | Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs Research Papers DOI | ||
11:15 15mTalk | Constraint Based Compiler Optimization for Energy Harvesting Applications Research Papers DOI | ||
11:30 15mTalk | Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises Research Papers Feiyang Jin Georgia Institute of Technology, Lechen Yu Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Georgia Institute of Technology, Jun Shirako Georgia Institute of Technology DOI | ||
11:45 15mTalk | On Leveraging Tests to Infer Nullable Annotations Research Papers Jens Dietrich Victoria University of Wellington, David J. Pearce ConsenSys, Mahin Chandramohan Oracle Labs DOI |