loading...
A Dynamic Logic for Deductive Verification of Concurrent Programs
London, England September 10-September 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.1Fifth IEEE International Conference o ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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

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
Usage of this product signifies your acceptance of the Terms of Use.