Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                            Vendredi 24 mai, 10h30

                                  Irene Yoon
                                 Inria Paris

               Velliris: A Relational Program Logic for LLVM IR

This talk introduces Velliris, a relational separation logic for LLVM IR in Coq.
VIR's formal semantics, using Interaction Trees (ITrees), provides a modular
and executable semantics for LLVM IR. It is equipped with a relational program
logic well-suited for control flow reasoning about possibly diverging programs.
However, most LLVM IR transformation passes not only modify the control flow;
their correctness also depends on invariants over state, using information
derived either from analysis passes or user annotations. In such context, the
pre-existing program logic of Interaction Trees falls short. In contrast, the
Iris framework offers a flexible way to construct language-specific separation
logics, which provide localized reasoning principles over state.
Velliris merges these approaches, defining a relational program logic in Iris
for the ITrees-defined VIR semantics. While typical Iris models build on small-step
operational semantics, we define a new weakest-precondition model for stateful
Interaction Trees to reconcile this approach. Moreover, we develop a robust
theory over LLVM IR resources, providing a novel way of specifying LLVM IR’s
attribute specifications, which record the compiler’s assumptions about
function calls.

            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.