Séminaire Cambium, Inria Paris
                                     BJ09
                         Vendredi 26 septembre, 10h30

                               Arthur Correnson

               Coinductive Proofs for Temporal (Hyper)Liveness

Temporal logics with explicit quantification over multiple traces have recently
been introduced as a powerful technique to specify hyperproperties of reactive
systems. Such logics can concisely express a wide range of interesting
hyperproperties, including subtle information-flow policies. However verifying
programs against them remains a challenge. This is particularly the case for
specifications with an alternation of universal and existential quantification
over system traces.

In this talk, we will present recent advancements in the interactive
verification of such ∀∃ temporal hyperproperties. We will first focus on the
verification of ∀∃ hyperproperties where the quantified traces are required to
satisfy a *safety* relation. We show that in this case, coinduction offers a
particularly intuitive proof technique. We will then discuss ongoing efforts to
adapt the approach to the case of *liveness* relations. These works have been
mechanized in the Rocq proof assistant, which raised a number of exciting
technical challenges related to Rocq's constructive nature.

The approaches presented in this talk are based on two recent publications:

- Coinductive Proofs for Temporal Hyperliveness (POPL 2025, with Bernd Finkbeiner)

- Almost Fair Simulations (ICFP 2025, with Iona Kuhn and Bernd Finkbeiner)

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.