Legals | KIT
Vladimir Klebanov

Dr. rer. nat. Vladimir Klebanov
Postdoctoral researcher

You have a problem with software reliability.
This is why you are here -
and this is why I am here.

KIT / Institute for Theoretical Computer Science
Am Fasanengarten 5
76131 Karlsruhe
Germany

Office 203
(Tel) +49 721 608 45252
(Fax) +49 721 608 44021
klebanov@kit.edu


News, Projects, Activities

CVE-2016-6313 - Bug in the Libgcrypt PRNG found with help of the Entroposcope tool

Entroposcope (new tool) - The first static analysis for finding bugs in PRNGs

Applying Formal Verification voted best elective CS master course of 2015 at KIT

VCLA International Student Award for outstanding undergraduate research for Felix Dörre's Bachelor thesis "Verification of Random Number Generators" supervised by Vladimir Klebanov

FTfJP 2016 (PC chair) - Workshop on Formal Techniques for Java-like Programs

VSTTE 2016 (PC member) - Verified Software: Theories, Tools, and Experiments

PSSV 2015 (PC member) - Workshop on Program Semantics, Specification and Verification: Theory and Applications

VSTTE 2015 (PC member) - Verified Software: Theories, Tools, and Experiments

VerifyThis @ ETAPS 2015 (co-organizer) - Verification Competition, London, Sunday, 12 April 2015

DeduSec (co-PI) - a DFG project within priority programme "Reliably Secure Software Systems (RS³)" (since October 2014)

IMPROVE (co-PI) - a DFG project within priority programme "Design for Future - Managed Software Evolution" (completed)

Dagstuhl Seminar 14171 (co-organizer) - Evaluating Software Verification Systems: Benchmarks and Competitions - April 22-25th, 2014

PSSV 2014 (PC member) - Workshop on Program Semantics, Specification and Verification: Theory and Applications

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) - IFIP Joint Intl. Conf. on Formal Techniques for Distributed Systems

VerifyThis 2012 (co-organizer) - Program Verification Competition at FM 2012

COMPARE2012 (PC co-chair) 1st Intl. Workshop on Comparative Empirical Evaluation of Reasoning Systems

PSSV 2012 (PC member) - Workshop on Program Semantics, Specification and Verification: Theory and Applications

COST IC0701 VerifyThis Verification Competition 2011 (co-organizer)

FoVeOOS 2011 (PC member) - 2nd Intl. Conference on Formal Verification of Object-oriented Software

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

2016

Felix Dörre and Vladimir Klebanov:
Entropy Loss and Output Predictability in the Libgcrypt PRNG (CVE-2016-6313)
PDF

Felix Dörre and Vladimir Klebanov:
Practical Detection of Entropy Loss in Pseudo-Random Number Generators
ACM Conference on Computer and Communications Security (CCS)
PDF (preprint)

Vladimir Klebanov (editor):
Proceedings, 18th Workshop on Formal Techniques for Java-like Programs (FTfJP 2016)
ACM DL

Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich:
Relational Program Reasoning Using Compiler IR
Verified Software: Theories, Tools, and Experiments (VSTTE)
To appear - Online tool

Vladimir Klebanov, Alexander Weigl, and Jörg Weisbarth:
Sound Probabilistic #SAT with Projection
Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL)
PDF (preprint)

2015

Felix Dörre and Vladimir Klebanov:
Pseudo-Random Number Generator Verification: A Case Study
Verified Software: Theories, Tools, and Experiments (VSTTE)
PDF (preprint) - BibTeX - LNCS 9593 - part of work recognized by the VCLA International Student Award

Bernhard Beckert, Vladimir Klebanov, and Mattias Ulbrich:
Regression Verification for Java Using a Secure Information Flow Calculus
Formal Techniques for Java-like Programs (FTfJP)
PDF - BibTeX - ACM DL

2014

Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich:
Information Flow in Object-Oriented Software
Logic-Based Program Synthesis and Transformation (LOPSTR 2013). Revised Selected Papers
PDF - BibTeX - Abstract - LNCS 8901

Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich:
Automating Regression Verification
Intl. Conference on Automated Software Engineering (ASE 2014)
PDF - BibTeX - ACM DL - Online tool

Vladimir Klebanov:
Precise Quantitative Information Flow Analysis - A Symbolic Approach
Theoretical Computer Science (TCS)
PDF - BibTeX - Abstract - ScienceDirect

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)
PDF - BibTeX - Abstract - LNCS 8054

2012

Vladimir Klebanov:
Precise Quantitative Information Flow Analysis Using Symbolic Model Counting
International Workshop on Quantitative Aspects in Security Assurance (QASA)
PDF - BibTeX - Note: this paper is superseded by the 2014 TCS paper

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
PDF