Sven Keidel

About Me

Portrait I am a computer science researcher, mathematician, and musician. I work as a researcher in the software technology group at TU Darmstadt in Germany.

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 (IDEs), continuous integration (CI) 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

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]

Activities

Reviewing

Research Projects

Sturdy

Sturdy Logo Sturdy is a Haskell library to create 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

Monto Logo As my master thesis project, I worked on Monto. Modern IDEs support multiple programming languages via plug-ins, but developing a high-quality language plug-in is a huge 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.

Teaching

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

Supervised Theses

Courses and Seminars

Contact

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

Office:
Hochschulstr. 10
64289 Darmstadt
Germany