Dr. Sven Keidel

Portrait I am a computer science researcher, mathematician, and musician. I work as a postdoc in the software technology group at TU Darmstadt in Germany. Prior to that, I worked as a PhD student at JGU Mainz under supervision of Prof. Sebastian Erdweg.

In my research, I develop techniques that simplify the design and implementation of static analyses. Static analyses are tools that provide information about programs by inspecting the source code without running them. They are used in integrated development environments, continuous integration servers, and compilers. A challenge in the design of such static analyses is to ensure that the analysis results are reliable (sound). However, rigorously proving that a static analysis is sound, is a difficult and laborious task. To this end, I develop techniques that simplify the development and soundness proof of static analyses. The core principle is to develop analyses from modular and reusable building blocks, such that the soundness proof becomes compositional.

Besides my main area of research, my research interests are proof techinques, category theory, type and effect systems. In my spare time I explore the vineyards of Mainz by bike and enjoy the nature. When I am at home, I like to play piano and bake delicious artisan sourdough bread.

Publications

Modular Specification and Compositional Soundness of Abstract Interpreters Sven Keidel.
PhD Dissertation. JGU Mainz, 2021. [pdf]
Grade Summa Cum Laude (with highest praise), received an award of the Dres. Göbel-Stiftung.

A Systematic Approach to Abstract Interpretation of Program Transformations
Sven Keidel and Sebastian Erdweg.
Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 2020. [pdf]

Sound and Reusable Components for Abstract Interpretation
Sven Keidel and Sebastian Erdweg.
Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, 2019 [pdf] [Talk]

Compositional Soundness Proofs of Abstract Interpreters
Sven Keidel, Casper Bach Poulsen and Sebastian Erdweg.
International Conference on Functional Programming (ICFP). ACM, 2018 [pdf] [Talk]

Toward Abstract Interpretation of Program Transformations
Sven Keidel and Sebastian Erdweg.
International Workshop on Meta-Programming Techniques and Reflection. ACM, 2017 [pdf]

The IDE Portability Problem and its Solution in Monto
Sven Keidel, Wulf Pfeiffer, and Sebastian Erdweg.
Proceedings of Software Language Engineering (SLE). ACM, 2016 [pdf**

Research Projects

OPAL is an analysis framework for Java with a focus on precision and scalability. Analyses in OPAL can be implemented modularly from loosely coupled modules. These modules do not call each other directly, but exchange information via a central data store called blackboard. A modular analysis implementation allows to replace modules to fine tune precision and scalability of the analysis.

Sturdy Logo Sturdy is a Haskell library to develop sound static analyses. Static analyses are tools that calculate information about programs. Soundness means that these information are correct and users can trust the results. However, proving that a static analysis for a real-world language is sound is difficult. Sturdy uses techniques for structuring static analyses such that their soundness proof becomes simpler.

Monto Logo Monto decouples editor services from their graphical front-end. In particular, modern IDEs support multiple programming languages via plug-ins. However, developing a high-quality language plug-in requires a considerable development effort and individual plug-ins are not reusable in other IDEs. This problem is called the IDE portability problem. Monto provides a solution to the IDE portability problem based on a language-independent and IDE-independent intermediate representation (IR) for editor services such as syntax highlighting, error messages, and code completion. This IR enables language services that support multiple IDEs with one plug-in.

Awards

Dissertation Award
JGU Mainz, 2022, Dres. Elke und Rainer Göbel-Stiftung.

Funding

DFG Grant: Correct, Efficient, and Flexible Fixpoint Algorithms for Big-Step Abstract Interpreters
Principled Investigator: Sebastian Erdweg, Coauthor: Sven Keidel
Deutsche Forschungs Gesellschaft (DFG) [project 451545561], 2021

Reviewing

Teaching

Lecturer and Organizer

Teaching Assistance

Supervision

PhD Students

Bachelor and Master Students

If you are looking for interesting and challenging bachelor and master thesis topics in the area of static analyses, please contact me.

Debugging Static Analyses in Sturdy
Tomislav Pree. Bachelor thesis. 2020, JGU Mainz. [pdf]

Type and Control-Flow Analysis for Scheme in Sturdy
Tobias Hombücher. Bachelor thesis. 2020, JGU Mainz. [pdf]

Soundness Proofs of Static Analyses in Coq
Jens de Waard. Master thesis. 2019, TU Delft. [pdf]

Sound Interprocedural Static Analysis for Stratego based on Regular Tree Grammars
Jente Hidskes. Master thesis. 2018, TU Delft. [pdf]

Sound Abstract Interpretation of JavaScript
Matthijs Bijman. Bachelor thesis. 2018, TU Delft. [pdf]

Sound Abstract Interpretation of Java
Wouter Raateland. Bachelor thesis. 2018, TU Delft. [pdf]

Interactive services in a disintegrated development environment
Hans Becker. Master thesis. 2017, TU Darmstadt. [pdf]

File dependencies in a disintegrated development environment
Stefan Kockmann. Bachelor thesis. 2016, TU Darmstadt. [pdf]

Activities

Contact

Email: sven.keidel@tu-darmstadt.de
GPG Key: 5142 E66C 2D02 EE31 8961 61D8 C023 6AA3 9E23 CB67

Office:
Hochschulstr. 10
64289 Darmstadt
Germany