• Home
• Team
  • Alumni/ae
    • Vladimir Klebanov
      • Publications
      • Teaching
      • Software
• Publications
• Tools
• Research
• Teaching
• Offers
• Media and News

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) - BibTeX - ACM DL

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)
PDF - BibTeX - LNCS 9971 - 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, updated) - BibTeX - EPTCS

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 - 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