Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning (Incorrectness 2024 - Formal Methods for Incorrectness 2024)

Sun 14 - Sat 20 January 2024 London, United Kingdom

Who

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Nat Karmios, Seung Hoon Park, Petar Maksimović, Philippa Gardner

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

Save

When

Tue 16 Jan 2024 11:00 - 11:22 at Mountbatten Exhibition - Logics and Program Analysis Chair(s): Noam Zilberstein

Abstract

We describe our recent work on unified compositional formal methods, meaning formalisms and tools that support both over-approximate compositional reasoning about program correctness (that is, verification) and under-approximate compositional reasoning about program incorrectness (that is, true bug-finding). Specifically, we discuss our unified compositional program logic exact separation logic and our new unified version of the compositional symbolic execution platform Gillian.

Link to Preprint

https://www.doc.ic.ac.uk/~aloow/papers/incorrectness24.pdf

Andreas Lööw

Imperial College London

Daniele Nantes-Sobrinho

Imperial College London

United Kingdom

Sacha-Élie Ayoun

Imperial College London

United Kingdom

Nat Karmios

Imperial College London

United Kingdom

Seung Hoon Park

Imperial College London

Petar Maksimović

Imperial College London, UK

Philippa Gardner

Imperial College London

United Kingdom

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

Display full programSpecify a time band

Save

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