Loops

I am co-organising a workshop in July 2025: Loop Invariants and Algebraic Reasoning (see here). To participate in-person, please register for the workshop through ICALP’s registration portal. To participate remotely over Zoom, please contact me for further details.

Workshop On Loop Invariants and Algebraic Reasoning

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. …

Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive …

Workshop On Reachability, Recurrences, and Loops