The goal of under-approximating logics (such as incorrectness separation logic) is to reason about the existence of bugs by specifying a subset of possible program behaviour. Specifically, an ISL triple says that any state in the post condition is reachable from some state in the precondition through executing the program in finitely many steps.

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, we will introduce a new approach, the \textit{forward under-approximating triple (FUA)} and its divergent variant. 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.

We will begin the presentation with an example program whose divergent behaviour cannot be captured by previously introduced logics, and show how FUA triples can reason about it. In the process, we will outline how FUA triples differ from traditional over-approximating and under-approximating approaches such as (partial) Hoare logic, exact separation logic, incorrectness (separation) logic and outcome logic. We will finish with a discussion of the mechanisms within the FUA framework that enable reasoning about divergence, with a focus on recursive functions and goto-cycles.

BSc Mathematics from Ruhr University Bochum. Worked on Exact Separation Logic during an internship with Philippa Gardner’s group at Imperial College London in 2021.
Currently studying English Literature at Vrije Universiteit Amsterdam.

This summer I worked on a new approach to prove non-termination bugs during an internship at Bloomberg LP under the supervision of Julien Vanegue and Azalea Raad.

The slides of my talk “The Never-Ending Trace”, held on January 16th, 2024, at the POPL Incorrectness Workshop, are uploaded to the workshop program, and can also be found on my LinkedIn profile, which is linked above!

Feel free to reach out to me anytime with questions, suggestions and feedback - I am always excited to talk about research! — c.cronjaeger@student.vu.nl —