Plenary talk by Sylvie Putot and Éric Goubault: Set-based methods in programs and systems verification

Sylvie Putot and Éric Goubault are professors at LIX, École Polytechnique, France.

This will be a survey talk on set-based methods we developed and used in program and (hybrid) systems analysis. 

We will first explain how abstract-interpretation based program validation is related to set-based methods ; we will exemplify this in particular with the affine arithmetic methods we developed over the last 12 years or so in the tool FLUCTUAT. 

Abstract interpretation computes program invariants, we need for that to enhance the set-based methods with least-fixed point computation methods. We will show how we dealt with it on affine arithmetic, and will mention some related topics, among which set-based constraint solving and characterization of invariants for continuous systems (to make a quick link to Daniel Wilczak’s invited tutorial).

One step beyond proving safety properties, using program invariants, is to consider temporal properties (in the sense of temporal logics). 

In order to prove these more general properties, we need not only outer-approximations of sets of reachable states, but also inner-approximations, parameterized by time. In our current work, in progress, we are deriving these outer and inner approximations on general hybrid systems, including a continuous part modeled by ODEs, from affine arithmetic, modal intervals and Taylor models. 

We will briefly show, if time permits, how to exploit these abstractions to verify or falsify general temporal properties.