Projects and Activities
COMPARE2012: 1st Intl. Workshop on Comparative Empirical Evaluation of Reasoning Systems
PSSV 2012: 3rd Workshop on Program Semantics, Specification and Verification: Theory and Applications
COST IC0701 Verification Competition 2011
FoVeOOS 2011: 2nd Intl. Conference on Formal Verification of Object-oriented Software
VSComp.org: The Verified Software Competition 2010
VerifyThis: A repository of OO program verification benchmarks
VerifyThus: A distribution of verification tools for OO languages
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
|
