Bi-Weekly Meeting: Carolina Gerlach

Wednesday, May 17, 2023, 10:30am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Carolina Gerlach

 

Abstract: 

Many interesting requirements, such as information-flow security policies, cannot be expressed as trace properties. Instead, security policies like noninterference are hyperproperties, which relate different executions of a system. Probabilistic hyperproperties express probabilistic relations between several independent executions of a system. Probabilistic hyperproperties can, for example, be expressed in HyperPCTL, which extends PCTL by quantification over states.

In this talk, I will give a gentle introduction to probabilistic hyperproperties, and present current work on an asynchronous extension of HyperPCTL, where the traces in different quantified computation trees do not have to evolve in lockstep anymore. This extension allows to capture the asynchronous nature of concurrent programs more accurately.