|
Dr. rer. nat. Vladimir Klebanov |
|
|
You have a problem with software reliability. |
KIT / Institute for Theoretical Computer Science
|
|
Projects and Activities
Dagstuhl Seminar 14171 (co-organizer) - Evaluating Software Verification Systems: Benchmarks and Competitions - April 21-25th, 2014
FTfJP 2013 (PC member) - Workshop on Formal Techniques for Java-Like Programs
PSSV 2013 (PC member) - Workshop on Program Semantics, Specification and Verification: Theory and Applications
ARiSVe 2013 (PC member) - Workshop on Automated Reasoning in Software Verification
STTT special section on program verification (guest editor)
FORTE/FMOODS 2013 (PC member)
VerifyThis 2012: Program Verification Competition at FM 2012 (co-organizer)
COMPARE2012: 1st Intl. Workshop on Comparative Empirical Evaluation of Reasoning Systems (co-organizer)
PSSV 2012: Workshop on Program Semantics, Specification and Verification: Theory and Applications (PC member)
COST IC0701 VerifyThis Verification Competition 2011 (co-organizer)
FoVeOOS 2011: 2nd Intl. Conference on Formal Verification of Object-oriented Software (PC member)
VSComp.org: The Verified Software Competition 2010 (participant, author)
VerifyThis: A repository of OO program verification benchmarks (originator)
VerifyThus: A distribution of verification tools for OO languages (originator)
Publications
2013
Vladimir Klebanov, Norbert Manthey, and Christian Muise:
SAT-based Analysis and Quantification of Information Flow in Programs
International Conference on Quantitative Evaluation of Systems (QEST 2013)
To appear.
2012
Vladimir Klebanov:
Precise Quantitative Information Flow Analysis Using Symbolic Model Counting
International Workshop on Quantitative Aspects in Security Assurance
(QASA)
PDF
- BibTeX
Bernhard Beckert, Vladimir Klebanov:
A Dynamic Logic for Deductive Verification of Multi-threaded Programs
Formal Aspects of Computing, special issue of revised papers
originally published in the International Conference on Software
Engineering and Formal Methods (SEFM)
PDF
- BibTeX
- Abstract
- SpringerLink
Vladimir Klebanov, Bernhard Beckert, Armin Biere, Geoff Sutcliffe:
Proceedings, 1st International Workshop on Comparative Empirical
Evaluation of Reasoning Systems (COMPARE 2012)
PDF
- BibTeX
- CEUR-WS 873
Marieke Huisman, Vladimir Klebanov, Rosemary Monahan:
On the Organisation of Program Verification Competitions
Proceedings, 1st International Workshop on Comparative Empirical
Evaluation of Reasoning Systems (COMPARE 2012)
PDF
- BibTeX
2011
Bernhard Beckert, Thorsten Bormer, Vladimir Klebanov:
Improving the Usability of Specification Languages and Methods for Annotation-based Verification
Post-proceedings, Intl. Symposium on Formal Methods for Components
and Objects (FMCO) 2010, Graz, Austria
PDF
- BibTeX
- Abstract
- LNCS
6957
V. Klebanov, P. Müller, N. Shankar,
G. T. Leavens, V. Wüstholz, E. Alkassar,
R. Arthan, D. Bronish, R. Chapman, E. Cohen,
M. Hillebrand, B. Jacobs, K. R. M. Leino,
R. Monahan, F. Piessens, N. Polikarpova,
T. Ridge, J. Smans, S. Tobies, T. Tuerk,
M. Ulbrich, and B. Weiß:
The 1st Verified Software Competition: Experience report.
17th International Symposium on Formal Methods (FM) 2011.
Winner Best Paper Award at FM 2011.
PDF
- BibTeX
- LNCS 6664
- Materials
2010
Daniel Bruns, Vladimir Klebanov, Ina Schaefer:
Verification of Software Product Lines with Delta-oriented Slicing
Revised Selected Papers, Intl. Conference on Formal Verification of Object-oriented Software (FoVeOOS) 2010, Paris
PDF
- BibTeX
- Abstract
- LNCS 6528
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