A Dynamic Logic for Deductive Verification of Concurrent Programs

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Bernhard Beckert Articles by Vladimir Klebanov

Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)

London, England

September 10-September 14

ISBN: 0-7695-2884-8

	ASCII Text	x
	Bernhard Beckert, Vladimir Klebanov, "A Dynamic Logic for Deductive Verification of Concurrent Programs," Software Engineering and Formal Methods, International Conference on, pp. 141-150, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007.

	BibTex	x
	@article{ 10.1109/SEFM.2007.1, author = {Bernhard Beckert and Vladimir Klebanov}, title = {A Dynamic Logic for Deductive Verification of Concurrent Programs}, journal ={Software Engineering and Formal Methods, International Conference on}, volume = {0}, year = {2007}, isbn = {0-7695-2884-8}, pages = {141-150}, doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.1}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Software Engineering and Formal Methods, International Conference on TI - A Dynamic Logic for Deductive Verification of Concurrent Programs SN - 0-7695-2884-8 SP141 EP150 A1 - Bernhard Beckert, A1 - Vladimir Klebanov, PY - 2007 KW - null VL - 0 JA - Software Engineering and Formal Methods, International Conference on ER -

Bernhard Beckert, University of Koblenz-Landau

Vladimir Klebanov, University of Koblenz-Landau

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.1

In this paper, we present an approach aiming at full functional deductive verification of concurrent Java programs, based on symbolic execution. We define a Dynamic Logic and a deductive verification calculus for a restricted fragment of Java with native concurrency primitives. Even though we cannot yet deal with non-atomic loops, employing the technique of symmetry reduction allows us to verify unbounded systems.

The calculus has been implemented within the KeYsystem, and we demonstrate it by verifying a central method of the StringBuffer class from the Java standard library.

Citation:

Bernhard Beckert, Vladimir Klebanov, "A Dynamic Logic for Deductive Verification of Concurrent Programs," sefm, pp.141-150, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.