Time: Friday, Feb 7, 10:00
Room: 03-233
Title: Modular Differential Software Verification and Pattern-based Equivalence Checking - Two Techniques for Incremental Verification
Abstract:
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.
Speaker bio:
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.