BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260910T155837Z
UID:Seminar-NESTiD-1160@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Othon Michail:MAILTO:Othon.Michail@liverpool.ac.uk
DTSTART:20230126T160000
DTEND:20230126T170000
SUMMARY:Durham-Liverpool synergy Series
DESCRIPTION:Hagit Attiya: Preserving Hyperproperties when Using Concurrent Objects\n\nLinearizability, a consistency condition for concurrent objects, is known to preserve trace properties. This suffices for modular usage of concurrent objects in applications, deriving their safety properties from the abstract object they implement. However, other desirable properties, like average complexity and information leakage, are not trace properties. These *hyperproperties* are not preserved by linearizable concurrent objects, especially when randomization is used. This talk will discuss formal ways to specify concurrent objects that preserve hyperproperties and their relation with verification methods like forward / backward simulation. We will show that certain concurrent objects cannot satisfy such specifications, and describe ways to mitigate these limitations.\n\nThis is a joint work with Constantin Enea and Jennifer Welch.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1160
LOCATION:
END:VEVENT
END:VCALENDAR