loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)
A Dynamic Logic for Deductive Verification of Concurrent Programs
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, IEEE 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, IEEE 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, IEEE 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, IEEE 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.