El 27 de enero próximo, a las 12:00 en la Sala Ada Lovelace de la Facultad, organizado por el grupo de investigación LOREA, César Sánchez de IMDEA Software Institute dara la charla Temporal Logics for Hyperproperties.

César Sánchez is an Associate Research Professor at the IMDEA Software Institute and Investigador Cientifico at CSIC. Cesar received a PhD from Stanford University in 2007, and joined the IMDEA Software institute in 2008.  His broad research interests are in the applications of logic to computer science and formal methods for the reasoning an verification of computational systems. In particular, he interested in the increasing the expressive power of temporal logics systems and in runtime verification for the dynamic analysis of reactive systems.

Hyperproperties are properties of systems that require to reason simultaneous about multiple traces of the system under analysis. Examples include security policies such as noninterference, non-inference, observational determinism, declassification, etc and other properties like symmetry of schedulers and correctness of coding/decoding systems. However, most of these properties are typically expressed in an ad-hoc manner, instead of using an expressive logic or formal language and the corresponding reasonging systems.  Standard temporal logics, like LTL, CTL and CTL* can only refer to a single path at a time and cannot express many hyperproperties of interest. In this talk, I will present HyperLTL and HyperCTL* that extend LTL and CTL* with quantification over multiple paths.  I will discuss aspects of these logics, like model-checking, satisfiability and runtime verification, and recent extensions and possibilities for future research.