Hello, my name is Sven Keidel. I’m a researcher, mathematician, and musician. Hello, my name is Sven Keidel. I’m a researcher, mathematician, and musician.
I work as a researcher in the programming languages group at JGU Mainz. In particular, I research techniques how static analyses can be proven sound. 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 is sound is rather difficult. In my research, I develop techniques for structuring a static analyses such that the soundness proof becomes easier.
Besides my main area of research, static analysis and abstract interpretation, my research interests are proof techinques, category theory, and 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 play the piano and the guitar.
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]
Sturdy 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 is sound is rather difficult. Sturdy uses techniques for structuring static analyses such that their soundness proof becomes simpler.
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.
Soundness Proofs of Static Analyses in Coq
Jens de Waard. Master thesis. 2019, TU Delft.
Sound Interprocedural Static Analysis for Stratego based on Regular Tree Grammars
Jente Hidskes. Master thesis. 2018, TU Delft.
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]
Sven Keidel
Office: 03-126
Email: keidel@uni-mainz.de
GPG Key
Address:
Staudingerweg 9 d
55128 Mainz
Germany