Abstract
In this paper we discuss an assertional proof method for multi-threaded Java programs. The method extends the proof theory for sequential Java programs with a generalization of the Owicki/Gries interference freedom test to threads in Java.
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
Abraham, E., de Boer, F.S., de Roever, W.P., Steffen, M.: An assertion-based proof system for mutithreaded Java. Theoretical Computer Science 331 (2005)
Apt, K.R.: Ten years of Hoare logic: a survey — part I. ACM Transactions on Programming Languages and Systems 3(4), 431–483 (1981)
Apt, K.R.: Formal justification of a proof system for Communicating Sequential Processes. Journal of the ACM 30(1), 197–216 (1983)
Apt, K.R., Francez, N., de Roever, W.P.: A proof system for Communicating Sequential Processes. ACM Transactions on Programming Languages and Systems 2, 359–385 (1980)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
de Boer, F.S.: A WP-calculus for OO. In: Thomas, W. (ed.) ETAPS 1999 and FOSSACS 1999. LNCS, vol. 1578, Springer, Heidelberg (1999)
The Extended Static Checker for Java (ESC/Java). URL: http://secure.ucd.ie/products/opensource/ESCJava2
Gerth, R.T., de Roever, W.-P.: Proving monitors revisited: A first step towards verifying object oriented systems. Fundamenta informaticae IX, pp. 371–400. North-Holland, Amsterdam (1986)
Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report 75, Department of Computer Science, University of Toronto (1975)
Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL 2005. Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York (2005)
The Java Modeling Language (JML). URL of the JML home page: http://www.cs.iastate.edu/~leavens/JML
Owicki, S.: A consistent and complete deductive system for the verification of parallel programs. In: Proceedings of the eighth annual ACM symposium on Theory of computing, ACM Press, New York (1976)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatika 6, 319–340 (1976)
Tucker, J.V., Zucker, J.I.: Program Correctness over Abstract Data Types, with Error-State Semantics. CWI Monograph Series. Centre for Mathematics and Computer Science, vol. 6. North-Holland, Amsterdam (1988)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
de Boer, F.S. (2007). A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs. In: Bonsangue, M.M., Johnsen, E.B. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2007. Lecture Notes in Computer Science, vol 4468. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72952-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-72952-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72919-8
Online ISBN: 978-3-540-72952-5
eBook Packages: Computer ScienceComputer Science (R0)