Document Open Access Logo

On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper)

Authors João Mota , Marco Giunti , António Ravara

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.40.pdf
  • Filesize: 0.87 MB
  • 29 pages

Document Identifiers

Author Details

João Mota
  • NOVA LINCS and NOVA School of Science and Technology, Caparica, Portugal
Marco Giunti
  • NOVA LINCS and NOVA School of Science and Technology, Caparica, Portugal
  • School of Computing, Engineering & Digital Technologies, Teesside University, Middlesbrough, UK
António Ravara
  • NOVA LINCS and NOVA School of Science and Technology, Caparica, Portugal

Funding

Partially supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No. 778233 (BehAPI) and NOVA LINCS (UIDB/04516/2020).
  • Mota, João: Partially supported by FCT.IP (2021.05297.BD).
  • Giunti, Marco: Partially supported by Dstl, reference: ACC2028868.

Acknowledgements

We would like to thank several members of the developer teams for the detailed responses and enlightening discussions, in particular, Bart Jacobs (VeriFast), Marieke Huisman (VerCors), Lukas Armborst (VerCors), Reiner Hähnle (KeY), Eduard Kamburjan (KeY), and Richard Bubel (KeY). Their feedback was indispensable for the development of this study.

Cite AsGet BibTex

João Mota, Marco Giunti, and António Ravara. On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 40:1-40:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.40

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
  • Theory of computation → Logic and verification
  • Theory of computation → Separation logic
Keywords
  • Java
  • Typestates
  • VeriFast
  • VerCors
  • Plural
  • KeY

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors. Deductive Software Verification - The KeY Book - From Theory to Practice, volume 10001 of Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-49812-6.
  2. Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos. Polymorphic lambda calculus with context-free session types. Inf. Comput., 289(Part A), 2022. URL: https://doi.org/10.1016/j.ic.2022.104948.
  3. Davide Ancona et al. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  4. Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara. A Java typestate checker supporting inheritance. Sci. Comput. Program., 221, 2022. URL: https://doi.org/10.1016/j.scico.2022.102844.
  5. Bernhard Beckert and Reiner Hähnle. Reasoning and Verification: State of the Art and Current Trends. IEEE Intell. Syst., 29(1):20-29, 2014. URL: https://doi.org/10.1109/MIS.2014.3.
  6. Nels E. Beckman. Modular typestate checking in concurrent Java programs. In Companion to the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 737-738. ACM, 2009. URL: https://doi.org/10.1145/1639950.1639990.
  7. Nels E. Beckman, Kevin Bierhoff, and Jonathan Aldrich. Verifying correct usage of atomic blocks and typestate. In Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 227-244. ACM, 2008. URL: https://doi.org/10.1145/1449764.1449783.
  8. Jan A. Bergstra and Jan Willem Klop. Process Algebra for Synchronous Communication. Inf. Control., 60(1-3):109-137, 1984. URL: https://doi.org/10.1016/S0019-9958(84)80025-X.
  9. Kevin Bierhoff and Jonathan Aldrich. Lightweight object specification with typestates. In Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 217-226. ACM, 2005. URL: https://doi.org/10.1145/1081706.1081741.
  10. Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 301-320. ACM, 2007. URL: https://doi.org/10.1145/1297027.1297050.
  11. Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek, and Alina Zolotukhina. Exogenous coordination of concurrent software components with JavaBIP. Softw. Pract. Exp., 47(11):1801-1836, 2017. URL: https://doi.org/10.1002/spe.2495.
  12. Simon Bliudze, Petra van Den Bos, Marieke Huisman, Robert Rubbens, and Larisa Safina. JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java. In 26th International Conference on Fundamental Approaches to Software Engineering, 2023. Google Scholar
  13. Stefan Blom, Saeed Darabi, Marieke Huisman, and Wytse Oortwijn. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In Proceedings of Integrated Formal Methods, volume 10510 of Lecture Notes in Computer Science, pages 102-110. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66845-1_7.
  14. Stefan Blom and Marieke Huisman. Witnessing the elimination of magic wands. Int. J. Softw. Tools Technol. Transf., 17(6):757-781, 2015. URL: https://doi.org/10.1007/s10009-015-0372-3.
  15. Stefan Blom, Marieke Huisman, and Marina Zaharieva-Stojanovski. History-Based Verification of Functional Behaviour of Concurrent Programs. In Radu Calinescu and Bernhard Rumpe, editors, Software Engineering and Formal Methods - 13th International Conference, Proceedings, volume 9276 of Lecture Notes in Computer Science, pages 84-98. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22969-0_6.
  16. Jan Boerman, Marieke Huisman, and Sebastiaan J. C. Joosten. Reasoning About JML: Differences Between KeY and OpenJML. In Integrated Formal Methods - 14th International Conference, Proceedings, volume 11023 of Lecture Notes in Computer Science, pages 30-46. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98938-9_3.
  17. Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In The 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 259-270, 2005. URL: https://doi.org/10.1145/1040305.1040327.
  18. John Boyland. Checking Interference with Fractional Permissions. In Static Analysis, 10th International Symposium, Proceedings, volume 2694 of Lecture Notes in Computer Science, pages 55-72. Springer, 2003. URL: https://doi.org/10.1007/3-540-44898-5_4.
  19. Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov, Hans Hüttel, Mathias Jakobsen, Mikkel Kettunen, and António Ravara. Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. In Asian Symposium on Programming Languages and Systems, volume 12470 of Lecture Notes in Computer Science, pages 105-124. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64437-6_6.
  20. Daniel Bruns, Wojciech Mostowski, and Mattias Ulbrich. Implementation-level verification of algorithms with KeY. Int. J. Softw. Tools Technol. Transf., 17(6):729-744, 2015. URL: https://doi.org/10.1007/s10009-013-0293-y.
  21. Yoonsik Cheon and Ashaveena Perumandla. Specifying and Checking Method Call Sequences in JML. In Hamid R. Arabnia and Hassan Reza, editors, Proceedings of the International Conference on Software Engineering Research and Practice, volume 2, pages 511-516. CSREA Press, 2005. Google Scholar
  22. David R. Cok. JML and OpenJML for Java 16. In FTfJP 2021: 23rd ACM International Workshop on Formal Techniques for Java-like Programs, 2021, Proceedings, pages 65-67. ACM, 2021. URL: https://doi.org/10.1145/3464971.3468417.
  23. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  24. Robert DeLine and Manuel Fähndrich. Typestates for Objects. In 18th European Conference on Object-Oriented Programming, Proceedings, volume 3086 of Lecture Notes in Computer Science, pages 465-490. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24851-4_21.
  25. José Duarte and António Ravara. Retrofitting Typestates into Rust. In 25th Brazilian Symposium on Programming Languages, pages 83-91. ACM, 2021. URL: https://doi.org/10.1145/3475061.3475082.
  26. Catarina Gamboa, Paulo Alexandre Santos, Christopher Steven Timperley, and Alcides Fonseca. User-driven Design and Evaluation of Liquid Types in Java. CoRR, abs/2110.05444, 2021. URL: https://arxiv.org/abs/2110.05444.
  27. David Harel. Dynamic logic. In Handbook of philosophical logic, pages 497-604. Springer, 1984. Google Scholar
  28. David Harel. Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Program., 8(3):231-274, 1987. URL: https://doi.org/10.1016/0167-6423(87)90035-9.
  29. Hans-Dieter A. Hiep, Jinting Bian, Frank S. de Boer, and Stijn de Gouw. A Tutorial on Verifying LinkedList Using KeY. In Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, volume 12345 of Lecture Notes in Computer Science, pages 221-245. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64354-6_9.
  30. Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  31. J.P. Hollander. Verification of a model checking algorithm in VerCors, August 2021. URL: http://essay.utwente.nl/88268/.
  32. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language Primitives and Type Discipline for Structured Communication-Based Programming. In Proceedings of Programming Languages and Systems, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  33. Marieke Huisman and Raúl E. Monti. On the Industrial Application of Critical Software Verification with VerCors. In Proceedings of Leveraging Applications of Formal Methods, volume 12478 of Lecture Notes in Computer Science, pages 273-292. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_18.
  34. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  35. Reiner Hähnle. Private communication, July 2022. Google Scholar
  36. Bart Jacobs. Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs. In Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, Proceedings, volume 12476 of Lecture Notes in Computer Science, pages 509-524. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61362-4_29.
  37. Bart Jacobs. Private communication, March 2022. Google Scholar
  38. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods - Third International Symposium, Proceedings, volume 6617 of Lecture Notes in Computer Science, pages 41-55. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-20398-5_4.
  39. Bart Jacobs, Jan Smans, and Frank Piessens. A Quick Tour of the VeriFast Program Verifier. In Programming Languages and Systems - 8th Asian Symposium, Proceedings, volume 6461 of Lecture Notes in Computer Science, pages 304-311. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17164-2_21.
  40. Ioannis T. Kassios. Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Proceedings, volume 4085 of Lecture Notes in Computer Science, pages 268-283. Springer, 2006. URL: https://doi.org/10.1007/11813040_19.
  41. Taekgoo Kim, Kevin Bierhoff, Jonathan Aldrich, and Sungwon Kang. Typestate protocol specification in JML. In Proceedings of the 8th International Workshop on Specification and Verification of Component-Based Systems, pages 11-18. ACM, 2009. URL: https://doi.org/10.1145/1596486.1596490.
  42. Sophie Lathouwers and Marieke Huisman. Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers. In 10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2022, pages 69-79. ACM, 2022. URL: https://doi.org/10.1145/3524482.3527652.
  43. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes, 31(3):1-38, 2006. URL: https://doi.org/10.1145/1127878.1127884.
  44. K Rustan M Leino and Peter Müller. A basis for verifying multi-threaded programs. In European Symposium on Programming, pages 378-393. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_27.
  45. K Rustan M Leino, Peter Müller, and Jan Smans. Verification of concurrent programs with Chalice. In Foundations of Security Analysis and Design V, pages 195-222. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03829-7_7.
  46. Bertrand Meyer. Applying 'design by contract'. Computer, 25(10):40-51, 1992. URL: https://doi.org/10.1109/2.161279.
  47. João Mota, Marco Giunti, and António Ravara. Java Typestate Checker. In Proc. of Coordination Models and Languages (COORDINATION), volume 12717 of Lecture Notes in Computer Science, pages 121-133. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-78142-2_8.
  48. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Proceedings of Verification, Model Checking, and Abstract Interpretation, volume 9583 of Lecture Notes in Computer Science, pages 41-62. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49122-5_2.
  49. Oscar Nierstrasz. Regular types for active objects. ACM sigplan Notices, 28(10):1-15, 1993. Google Scholar
  50. Peter O'Hearn. Resources, concurrency, and local reasoning. Theoretical computer science, 375(1-3):271-307, 2007. URL: https://doi.org/10.1016/j.tcs.2006.12.035.
  51. Peter O'Hearn, John Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In International Workshop on Computer Science Logic, pages 1-19. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  52. Wytse Hendrikus Marinus Oortwijn. Deductive techniques for model-based concurrency verification. PhD thesis, University of Twente, 2019. Google Scholar
  53. Matthew J. Parkinson and Alexander J. Summers. The Relationship between Separation Logic and Implicit Dynamic Frames. In Proceedings of Programming Languages and Systems, volume 6602 of Lecture Notes in Computer Science, pages 439-458. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19718-5_23.
  54. Willem Penninckx, Bart Jacobs, and Frank Piessens. Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. In Programming Languages and Systems, Proceedings, volume 9032 of Lecture Notes in Computer Science, pages 158-182. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_7.
  55. John C Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74. IEEE, 2002. URL: https://doi.org/10.1109/lics.2002.1029817.
  56. R.B. Rubbens. Improving Support for Java Exceptions and Inheritance in VerCors. Master’s thesis, University of Twente, 2020. URL: http://essay.utwente.nl/81338/.
  57. Ayesha Sadiq, Yuan-Fang Li, and Sea Ling. A survey on the use of access permission-based specifications for program verification. Journal of Systems and Software, 159, 2020. URL: https://doi.org/10.1016/j.jss.2019.110450.
  58. Jan Smans, Bart Jacobs, Frank Piessens, and Wolfram Schulte. An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. In Fundamental Approaches to Software Engineering, 11th International Conference, Held as Part of the Joint European Conferences on Theory and Practice of Software, Proceedings, volume 4961 of Lecture Notes in Computer Science, pages 261-275. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78743-3_19.
  59. Robert E. Strom and Shaula Yemini. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Trans. Software Eng., 12(1):157-171, 1986. URL: https://doi.org/10.1109/TSE.1986.6312929.
  60. André Trindade, João Mota, and António Ravara. Typestates to Automata and back: a tool. In Proceedings 13th Interaction and Concurrency Experience, ICE 2020, volume 324 of EPTCS, pages 25-42, 2020. URL: https://doi.org/10.4204/EPTCS.324.4.
  61. André Trindade, João Mota, and António Ravara. Typestate Editor. https://typestate-editor.github.io/, 2022.
  62. Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer. GhostCell: Separating Permissions from Data in Rust. Proc. ACM Program. Lang., 5(ICFP):1-30, 2021. URL: https://doi.org/10.1145/3473597.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact