Dr. Benjamin Weiß

benjamin(dot)weiss ∂does-not-exist.alumni(dot)uni-karlsruhe(dot)de

Projects
Title
KeY
COST Action IC0701

Software

KeY	- the KeY verification tool for Java programs
KeYHeap	- a major revision of KeY based on a different way of modelling heap memory

Publications
Title	Author(s)	Source
Predicate Abstraction in a Program Logic Calculus	Benjamin Weiß	Science of Computer Programming 76 (10), Elsevier, 2011
The 1st Verified Software Competition: Experience Report	Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß	17th International Symposium on Formal Methods (FM 2011), Limerick, Ireland. LNCS 6664, Springer, 2011. Best paper award at FM 2011.
Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction	Benjamin Weiß	PhD thesis, Karlsruhe Institute of Technology. KIT Scientific Publishing, 2011
Dynamic Frames in Java Dynamic Logic	Peter H. Schmitt Mattias Ulbrich Benjamin Weiß	International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. LNCS 6528, Springer, 2011
Abstract Interpretation of Symbolic Execution with Explicit State Updates	Richard Bubel Reiner Hähnle Benjamin Weiß	7th International Symposium on Formal Methods for Components and Objects (FMCO 2008), Sophia Antipolis, France. LNCS 5751, Springer, 2009
Verification of Modifies Clauses in Dynamic Logic with Non-rigid Functions	Christian Engel Andreas Roth Peter H. Schmitt Benjamin Weiß	Technical Report 2009-9, Department of Computer Science, University of Karlsruhe, 2009
Predicate Abstraction in a Program Logic Calculus	Benjamin Weiß	7th International Conference on integrated Formal Methods (iFM 2009), Düsseldorf, Germany. LNCS 5423, Springer, 2009
Inferring Invariants by Symbolic Execution	Peter H. Schmitt Benjamin Weiß	4th International Verification Workshop (VERIFY'07), Workshop at CADE-21, Bremen, Germany, 2007

Minor and Diploma Thesis
Title	Type	Supervisor	Year
Inferring Invariants by Static Analysis in KeY	Diplomarbeit	Prof. P. H. Schmitt	2007
Statically Checking Encapsulation in KeY with the Universe Type System	Studienarbeit	Prof. P. H. Schmitt Andreas Roth	2006

Teaching
Title	Type
Formale Entwicklung objektorientierter Software (WS 10/11)	Praktikum
Formale Programmentwicklung (SS 10)	Seminar
Formale Entwicklung objektorientierter Software (WS 09/10)	Praktikum
Formale Programmentwicklung (SS 09)	Seminar
Formale Entwicklung objektorientierter Software (WS 08/09)	Praktikum
Formale Software-Entwicklung (SS 08)	Seminar
Formale Entwicklung objektorientierter Software (WS 07/08)	Praktikum
Formale Software-Entwicklung (SS 07)	Seminar

Supervised Theses
Title	Type	Author	Year
Funktionsabschlüsse in Dynamischer Logik	Studienarbeit	Gregor Bethlen	2010
Specifying Selected Parts of the Java API Using Dynamic Frames	Studienarbeit	Daniel Peters	2010
A Calculus for Data Abstraction	Diplomarbeit	Roman Krenický	2009
Formal Semantics for the Java Modeling Language	Diplomarbeit	Daniel Bruns	2009
Verification of Java Floating-Point Arithmetic	Diplomarbeit	Denis Lohner	2008
Verification of Sun SPOT's Network Library	Diplomarbeit	Christoph Scheben	2008