Abstract
Reasoning about object-oriented programs is hard, due to aliasing, dynamic binding and the need for data abstraction and framing. Reasoning about concurrent object-oriented programs is even harder, since in general interference by other threads has to be taken into account at each program point.
In this paper, we propose an approach to the automatic verification of concurrent Java-like programs. The cornerstone of the approach is a programming model, a set of rules, which limits thread inference to synchronization points such that one can reason sequentially about most code. In particular, programs conforming to the programming model are guaranteed to be data race free. Compared to previous incarnations of the programming model, our approach is more flexible in describing the set of memory locations protected by an object’s lock. In addition, we combine the model with an approach for data abstraction and framing based on dynamic frames. To the best of our knowledge, this is the first paper combining dynamic frames and concurrency.
We implemented the approach in a tool, called VeriCool, and used it to verify several small concurrent programs.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Gosling, J., Joy, B., Steele, G., Bracha, G.: The java language specification, 3rd edn. (2005)
Jacobs, B., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. In: SAVCBS (2004)
Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: SEFM (2005)
Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: ICFEM (2006)
Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for java-like programs based on dynamic frames (2008)
Kassios, Y.: A Theory of Object Oriented Refinement. PhD thesis, University of Toronto (2006)
Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: ESOP (2008)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3) (2007)
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: APLAS (2007)
Haack, C., Hurlin, C.: Separation logic contracts for a java-like language with fork/join. Technical Report 6430, INRIA (2008)
DeLine, R., Leino, K.R.M.: Boogiepl: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-, -70 (2005)
Leino, K.R.M., Schulte, W.: A verifying compiler for a multi-threaded object-oriented language. In: Marktoberdorf Summer School Lecture Notes (2006)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI (2002)
Leino, K.R.M., Nelson, G., Saxe, J.B.: Esc/java user’s manual. Technical Report SRC-TN-2000-002, Compaq Research Center (2000)
Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: SAS (2007)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO (2005)
Ábrahám Mumm, E., de Boer, F.S., de Roever, W.P., Steffen, M.: Verification for java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol. 2303, Springer, Heidelberg (2002)
Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA (2002)
Hoare, C.: Monitors: An operating system structuring concept. cacm 17(10) (1974)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smans, J., Jacobs, B., Piessens, F. (2008). VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language. In: Barthe, G., de Boer, F.S. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2008. Lecture Notes in Computer Science, vol 5051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68863-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-68863-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68862-4
Online ISBN: 978-3-540-68863-1
eBook Packages: Computer ScienceComputer Science (R0)