Hoare-Like Triples and Kleene Algebras with Top and Tests (Incorrectness 2024 - Formal Methods for Incorrectness 2024) - POPL 2024

Sun 14 - Sat 20 January 2024 London, United Kingdom

Who

Lena Verscht, Benjamin Lucien Kaminski

Track

Incorrectness 2024

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Tue 16 Jan 2024 12:07 - 12:30 at Mountbatten Exhibition - Logics and Program Analysis Chair(s): Noam Zilberstein

Abstract

We aim at a holistic perspective on program logics, including Hoare and incorrectness logics. To this end, we study different classes of properties arising from the generalization of the aforementioned logics. We compare our results with the properties expressible in the language of Kleene algebra with top and tests.

Link to Preprint

https://arxiv.org/abs/2312.09662

File attachments

Slides (slides.pdf)	466KiB

Lena Verscht

Saarland University, Saarland Informatics Campus

Benjamin Lucien Kaminski

Saarland University; University College London

Germany

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Tue 16 Jan
Displayed time zone: London change

	11:00 - 12:30	Logics and Program AnalysisIncorrectness at Mountbatten Exhibition Chair(s): Noam Zilberstein Cornell University

	11:00 22m Talk		Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning Incorrectness Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Nat Karmios Imperial College London, Seung Hoon Park Imperial College London, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London Pre-print
	11:22 22m Talk		The Never-Ending Trace: An Under-Approximate Approach to Divergence Bugs Incorrectness Caroline Cronjäger Vrije Universiteit Amsterdam Pre-print
	11:45 22m Talk		Work in Progress: Modelling Incorrect Programs in the Open World with Dafny Incorrectness James Noble Creative Research & Programming, Tobias Wrigstad Uppsala University, Susan Eisenbach Imperial College London File Attached
	12:07 22m Talk		Hoare-Like Triples and Kleene Algebras with Top and Tests Incorrectness Lena Verscht Saarland University, Saarland Informatics Campus, Benjamin Lucien Kaminski Saarland University; University College London Pre-print File Attached