Vladimir Klebanov, KeY project

Vladimir Klebanov
KIT
Institute for Theoretical Computer Science
Am Fasanengarten 5
76131 Karlsruhe
Germany
(Tel) +49 721 608 5252
(Fax) +49 721 608 xxxx

Please use the old email address so far:
vladimir@uni-koblenz.de

Affiliations

• The KeY project (intranet)
  
• Local research group
  
• My boss: Bernhard Beckert
  
• COST Action IC0701

Research interests

• Software verification
• Dynamic Logic for Java
• Concurrency and Verification
• Theorem prover UI

On a lighter note

• my flickr
• breviary
• daily dose
•  Sweden blog 2006

2009

Vladimir Klebanov:
Extending the Reach and Power of Deductive Program Verification
Doctoral dissertation, Department of Computer Science, Universität Koblenz-Landau
PDF - Cartoon summary

Bernhard Beckert, Thorsten Bormer, Vladimir Klebanov:
On Essential Program Annotations and Completeness of Verifying Compilers
Workshop on Verified Software: Theory, Tools, and Experiments (VSTTE) 2009, Eindhoven, The Netherlands
PDF - BibTeX - Abstract

2008

Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer:
Integrating Verification and Testing of Object-Oriented Software
Tutorial, Second International Conference on Tests and Proofs (TAP) 2008, Prato, Italy
PDF - BibTeX - Abstract - LNCS 4966

2007

Bernhard Beckert and Vladimir Klebanov:
A Dynamic Logic for Deductive Verification of Concurrent Java Programs With Condition Variables
1st International Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP) 2007, Lisbon, Portugal
PDF - BibTeX - Abstract

Bernhard Beckert and Vladimir Klebanov:
A Dynamic Logic for Deductive Verification of Concurrent Programs
Software Engineering and Formal Methods (SEFM) 2007, London, UK
PDF - BibTeX - Abstract

Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov,
Philipp Rümmer, Steffen Schlager, Peter H. Schmitt:
The KeY System 1.0 (Deduction Component) (system description)
21st Conference on Automated Deduction (CADE-21), Bremen, Germany, 2007
PDF - BibTeX - Abstract - LNCS 4603

- Bernhard Beckert, Vladimir Klebanov and Steffen Schlager: Dynamic Logic (Chapter 3)
- Vladimir Klebanov: Proof Reuse (Chapter 13)
in: Verification of Object-Oriented Software: The KeY Approach, Springer LNCS 4334
BibTeX (the book) - Springerlink - Amazon.de

2006

Bernhard Beckert and Vladimir Klebanov:
Must Program Verification Systems and Calculi be Verified? (discussion paper)
3rd International Verification Workshop - VERIFY'06, Seattle, USA
PDF - BibTeX - Abstract

2005

Bernhard Beckert, Thorsten Bormer, Vladimir Klebanov:
Reusing Proofs when Program Verification Systems are Modified (position paper)
Software Certificate Management Workshop (SoftCeMent) 2005, Long Beach, USA
PDF - BibTeX - Abstract

V. Klebanov, Ph. Rümmer, St. Schlager, P.H. Schmitt: Verification of JCSP Programs.
Communicating Process Architectures (CPA) 2005, Eindhoven, The Netherlands
PDF - BibTeX - Abstract

2004

Vladimir Klebanov: A JMM-Faithful Non-Interference Calculus for Java.
FIDJI 2004 Workshop on Scientific Engineering of Distributed Java Applications, Luxembourg.
PDF - BibTeX - Abstract - Springer LNCS 3409

Bernhard Beckert and Vladimir Klebanov: Proof Reuse for Deductive Program Verification.
Software Engineering and Formal Methods (SEFM) 2004, Beijing, China.
PDF - BibTeX - Abstract - Pics

Bernhard Beckert and Vladimir Klebanov: Proof Reuse for Program Verification Calculi.
Extended Abstract. Contributions to the IJCAR DP 2004, Cork, Ireland,
CEUR Workshop Proceedings, ISSN 1613-0073, online copy.

2003

Vladimir Klebanov: Proof Re-Use in Java Software Verification
Diploma thesis, University of Karlsruhe, Supervisor: Bernhard Beckert
PDF