Please contact Sebastian Erdweg if interested.
Sebastian Erdweg of the Programming Languages research group received the Most Influential Paper Award for his 2011 OOPSLA paper on SugarJ.
The award is presented by ACM SIGPLAN to the authors of the paper that had the most impact in the previous 10 years.
Persistent Software Transactional Memory in Haskell
Nicolas Krauter, Patrick Raaf, Peter Braam, Reza Salkhordeh, Sebastian Erdweg, Andre Brinkmann. In Proceedings of the ACM on Programming Languages (ICFP). ACM, 2021
A Systematic Approach to Deriving Incremental Type Checkers
André Pacak, Sebastian Erdweg, and Tamás Szabó,. In Proceedings of the ACM on Programming Languages (OOPSLA). ACM, 2020. [ pdf ]
Time: Friday, Feb 7, 10:00
Title: Modular Differential Software Verification and Pattern-based Equivalence Checking - Two Techniques for Incremental Verification
In this talk, I will give an overview on our current work in the area of incremental verification. The talk will consist of two parts. In the first part, I will present work in progress on modular differential software verification. Its basic idea is to restrict reverification to the modified program paths. I will explain how we identify the modified program paths and how we leverage conditional model checking to restrict verification to those modified program paths. In the second part, I will talk about our ideas on checking functional equivalence for parallelized program and how we want to make use of parallelization patterns.
Marie-Christine Jakobs is assistant professor at the TU Darmstadt leading the Semantics and Verification of parallel Systems group. She studied computer science at Paderborn University, where she also did her doctorate. From 2017 to 2019 she worked as postdoctoral researcher at LMU Munich. Her research focus is on theoretical results and practical approaches for automatic software verification. For example, she is one of the developers of the software verification framework CPAchecker. Currently, she is interested in incremental verification, the combination of verification approaches, test-case generation with verifiers, and the validation of verification results.