During and after my bachelor's degree in mathematics and computer science I have worked on verification and program logics through multiple research internships. While working at Imperial College London in 2021, I worked on the soundness proof of under-approximate reasoning about function calls, and co-authored a paper on Exact Separation Logic. My most recent work focuses on providing a logic that can prove the existence on non-terminating execution traces without false-positive bug reports. I get excited about proofs and all things mathy.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Saarbrücken

The goal of under-approximating logics, such as incorrectness logic, is to reason about the existence of bugs  by specifying a subset of possible program behaviour. While this approach allows for the specification of a broad range of bugs, it does not account for divergence bugs (such as infinite loops), since the nature of the triple itself does not allow statements about infinite execution traces.  
 
To fill this gap, I will present a divergent variant of the forward under-approximating (FUA) triple. This new separation logic reasons functionally compositionally about divergence bugs and is under-approximating in the sense that all specified bugs are true bugs, that is, reachable. It can detect divergence originating from loops, recursive function calls and goto-cycles.  
 
I will motivate the talk by defining the type of divergent programs we are aiming to reason about, and show how previously introduced logics fall short of specifying their divergent behaviour. After introducing the FUA triple, I will outline how this triple differs from traditional over-approximating  and under-approximating approaches such as (partial) Hoare logic and incorrectness logic. Finally, I will discuss the mechanisms within the FUX framework that enable reasoning about divergence, with a focus on how to prove divergence arising from goto-cycles.

--

Please contact the office team for the Zoom link details.

Annika Meiser

+49 681 9303 9105

--email hidden

Yes

Kaiserslautern

G26

607

-