 |
|
|
| Researcher
Room: 229 Phone: +49 721 608-44338 Fax: +49 721 608-44021 ulbrich@kit.edu |
Am Fasanengarten 5 Gebäude 50.34 76131 Karlsruhe Germany |
|
Interests
My research focuses on formal deductive software verification on the level of program code. I am particularly intersted in relational verification, i.e., cases where more than one program is considered for the verification:
- Regression verification, equivalence checking
- Algorithm Refinement
- Verification of relational properties of algorithms
- Information Flow Security (to a lesser extend)
I am also interested in
- Intermediate Verification Languages and Interaction
- Dynamic Logic
Projects
JML Standard
Committees
- JML Workshop Bad Herrenalb, 2016, Co-organiser
- VSTTE 2017, PC member
- VerifyThis 2017, Co-organiser
- HFC 2017, PC member
Tools
- rêve - Automatically check two programs for equivalence
- rêve for noninterference - Automatically prove noninterference of a C routine
- SemSlice - Automatically semantic analysis for precise programs slicing
- Tableau Applet - A Java Applet for a first tableau calculus (w/ some automation), mainly for teaching purposes
- KeY - Integrated Deductive Software Design
- ivil - Interactive Verification on Intermediate Language
Recent Publications
Click here for a full list of my publications.
Supervised Theses
| Title | Year | Type |
|---|---|---|
| Specifying and Verifying Real-World Java Code with KeY - Case Study java.math.BigInteger | 2017 | B. Sc. |
| Semantic Slicing | 2016 | |
| Dynamic Analysis for Automatic Relational Verification | 2016 | B.Sc. |
| Dual Pivot Quicksort: Specification and Verification using KeY | 2016 | B.Sc. |
| Theory of Refinement of Cyber-Physical Systems into Implementations | 2015 | B.Sc. |
| Generating Bounded Counterexamples for KeY Proof Obligations | 2014 | M.Sc. |
| Automating Regression Verification | 2014 | |
| Proving Well-Definedness of JML Specifications with KeY | 2013 | M.Sc. |
| Design and Implementation of a Verification Framework for Java Bytecode using Unstructured Dynamic Logic | 2012 | DA |
| Introducing the Boogie methodology to USDL | 2011 | StA |
| Verifying Alloy Models Using KeY | 2011 | DA |
| Funktionsabschlüsse in Dynamischer Logik | 2010 | StA |
| Formal Semantics for the Java Modeling Language | 2009 | DA |
| Click here to show all supervised theses | ||
Teaching
| Title | Type |
|---|---|
| Formale Systeme II: Anwendung (SS 17) | Lehrbeauftragter |
| Formale Systeme (WS 16/17) | VL-Vertretungen |
| Formale Systeme II: Theorie (SS 16) | Lehrbeauftragter |
| Formale Systeme (WS 15/16) | Übung zur Vorlesung |
| Anwendung Formaler Verifikation (SS 15) | Lehrbeauftragter |
| Desaster in der Software-Sicherheit (WS 14/15) | Proseminar |
| Formale Systeme (WS 14/15) | Übung zur Vorlesung |
| Formale Systeme (WS 13/14) | Übung zur Vorlesung |
| Formale Systeme (WS 12/13) | Übung zur Vorlesung |
| Formale Systeme (WS 11/12) | Übung zur Vorlesung |
| 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 Systeme (WS 08/09) | Übung zur Vorlesung |
| Formale Software-Entwicklung (SS 08) | Seminar |
| Formale Systeme (WS 07/08) | Übung zur Vorlesung |
| Click here to show all teaching activities | |
