Viinistu, Estonia, March 4 - 7, 2024
Full Research Professor at the IMDEA Software Institute, Spain
Formal verification is the problem of a system satisfies a
specification. A common language to express behaviors is Linear
Temporal Logic (LTL) a modal logic to express temporal properties of
single traces of the execution of a system. A system satisfies an LTL
specification if all executions conform to it.
Hyperproperties are properties of systems that require to reason
simultaneously 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. Unfortunately, standard temporal logics,
like only refer to a single path at a time and cannot express many
hyperproperties of interest.
In these talks, I will revisit LTL with many examples and describe its
model checking problem. Then, I will introduce HyperLTL, which extends
LTL and with quantification over multiple paths. I will also show
many examples of properties in this logic, and then introduce model
checking algorithms, including a bounded model checking approach.
I will then present extension of HyperLTL for real-time and
asynchronous properties where the different traces of execution can
evolve at different speeds. Finally, I will present open problems and
current avenues for research.
About the speaker: 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. From the theory viewpoint, he is interested in the increasing the expressive power of temporal logics systems and in runtime verification for the dynamic analysis of reactive systems. His main practical interests are applications of runtime verification to autonomous systems and smart-contract and blockchain reliability.
Last changed
March 7, 2024 9:35 EET (GMT +02:00)
by local organisers