SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Thu 8 Dec 2022 16:00 - 16:30 at Seminar Room G007 - Verification Chair(s): Dominique Devriese

Robust modules guarantee to do only what they are supposed to do – even in the presence of untrusted malicious clients, and considering not just the direct behaviour of individual methods, but also the emergent behaviour from calls to more than one method. Necessity is a language for specifying robustness, based on novel necessity operators capturing temporal implication, and a proof logic that derives explicit robustness specifications from functional specifications. Soundness and an exemplar proof are mechanised in Coq.

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
VerificationOOPSLA at Seminar Room G007
Chair(s): Dominique Devriese KU Leuven
15:30
30m
Talk
Checking Equivalence in a Non-strict Language
OOPSLA
John C. Kolesar Yale University, Ruzica Piskac Yale University, William T. Hallahan Yale University
DOI
16:00
30m
Talk
Necessity Specifications for Robustness
OOPSLA
Julian Mackay Victoria University of Wellington, Susan Eisenbach Imperial College London, James Noble Research & Programming, Sophia Drossopoulou Meta and Imperial College London
DOI
16:30
30m
Research paper
Quantitative strongest post: a calculus for reasoning about the flow of quantitative information
OOPSLA
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University and University College London
DOI