Dear all,
Next week, we have the pleasure of having Prof. Hagit Attiya give a talk in the colloquium.
The seminar will be held on Monday, May 27th at 14:00. Location: C220.
The title, abstract and bio appear below.
Looking forward to seeing you, Sagie and Liat
*Title:* Preserving Hyperproperties when Using Concurrent Objects
*Abstract:* Linearizability, 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. We will show that certain concurrent objects cannot satisfy such specifications, and describe ways to mitigate these limitations.
This is a joint work with Constantin Enea and Jennifer Welch.
*Bio*:
Hagit Attiya is a professor at the department of Computer Science at the Technion,
Israel Institute of Technology, and holds the Harry W. Labov and Charlotte Ullman Labov Academic Chair. She received all her academic degrees, in Computer Science, from the Hebrew University of Jerusalem, and was a post-doctoral fellow at MIT.
Reminder, this is happening today.
On Mon, May 20, 2024 at 3:47 PM Sagie Benaim sagie.benaim@mail.huji.ac.il wrote:
Dear all,
Next week, we have the pleasure of having Prof. Hagit Attiya give a talk in the colloquium.
The seminar will be held on Monday, May 27th at 14:00. Location: C220.
The title, abstract and bio appear below.
Looking forward to seeing you, Sagie and Liat
*Title:* Preserving Hyperproperties when Using Concurrent Objects
*Abstract:* Linearizability, 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. We will show that certain concurrent objects cannot satisfy such specifications, and describe ways to mitigate these limitations.
This is a joint work with Constantin Enea and Jennifer Welch.
*Bio*:
Hagit Attiya is a professor at the department of Computer Science at the Technion,
Israel Institute of Technology, and holds the Harry W. Labov and Charlotte Ullman Labov Academic Chair. She received all her academic degrees, in Computer Science, from the Hebrew University of Jerusalem, and was a post-doctoral fellow at MIT.
-
Sagie Benaim