Florian Lanzinger
| Florian Lanzinger, M.Sc. — Researcher / PhD Student | |
| Am Fasanengarten 5 Building 50.34 Office 227 76131 Karlsruhe Germany |
📞 + 49 721 608-43856 |
Projects
Publications
| Title | Author(s) | Source |
|---|---|---|
| The Java Verification Tool KeY: A Tutorial | Bernhard Beckert Richard Bubel Daniel Drodt Reiner Hähnle Florian Lanzinger Wolfram Pfeifer Mattias Ulbrich Alexander Weigl | 26th International Symposium on Formal Methods (FM 2024) |
| Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis | Florian Lanzinger Christian Martin Frederik Reiche Samuel Teuber Robert Heinrich Alexander Weigl | Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC 2024 |
| Title | Author(s) | Source |
|---|---|---|
| Scalable and Precise Refinement Types for Imperative Languages | Florian Lanzinger Joshua Bachmeier Mattias Ulbrich Werner Dietl | iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings |
| Title | Author(s) | Source |
|---|---|---|
| A Refactoring for Data Minimisation Using Formal Verification | Florian Lanzinger Mattias Ulbrich Alexander Weigl | 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA 2022) |
| The Karlsruhe Java Verification Suite | Jonas Klamroth Florian Lanzinger Wolfram Pfeifer Mattias Ulbrich | The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday |
| Towards a Formal Approach for Data Minimization in Programs | Florian Lanzinger Alexander Weigl | Data Privacy Management, Cryptocurrencies and Blockchain Technology |
| Title | Author(s) | Source |
|---|---|---|
| Scalability and Precision by Combining Expressive Type Systems and Deductive Verification | Florian Lanzinger Alexander Weigl Mattias Ulbrich Werner Dietl | Proceedings of the ACM on programming languages 5(OOPSLA) |
| Property Types in Java: Combining Type Systems and Deductive Verification | Florian Lanzinger | Karlsruher Institut für Technologie (February 2021) |
| Title | Author(s) | Source |
|---|---|---|
| A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification | Florian Lanzinger | Karlsruher Institut für Technologie (April 2018) |
Supervised Theses
| Title | Type | State | Student | Year |
|---|---|---|---|---|
| Closing the Gap between Models and Programs | MA / PdF | open | — | — |
| Dependent Types for Java | BA / MA | open | — | — |
| Modellierung von Angriffen für quantitative Sicherheitsanalysen | MA | open | — | — |
| Semantische Datenminimierung | open | — | — | |
| A Translation Layer for Information Flow Verification Systems: Bridging Type Systems with Theorem Prover | BA | finished | Felix Mühlenberend | 2023 |
| LiquidRust: Refinement Types for Imperative Languages with Ownership | MA | finished | Carsten Csiky | 2022 |
| Mutability for Property Types in Java | MA | finished | Joshua Bachmeier | 2022 |
| Abhängige Eigenschaftstypen in Java | BA | finished | Liudmila Fomenko | 2022 |
| Methode zur Datenminimierung mittels syntaktischer Programmpartitionierung | BA | finished | Simon Gerst | 2021 |
Teaching
| Course | Type | Semester |
|---|---|---|
| Basic Notions of Computer Science | Practice | Winter Term 2023/2024 |
| Application of Formal Methods | Seminar | Winter Term 2023/2024 |
| Application of Formal Methods | Seminar | Summer Term 2023 |
| Application of Formal Methods | Seminar | Summer Term 2021 |