Laure Gonnord, 18 nov. 2014

Assistant Professor since 2009

Univ Lille 1 / LIFL

since sept 2013 : Univ Lyon 1 / LIP

Numerical invariant generation for safety

Formal methods for Software Engineering

Reactive systems: synchronous design

Compilation: scheduling,

**termination**of programs

Reactive systems

Proving full correction

Because termination is related to scheduling

Given a program

```
//N>0
i = N;
while(i>0)
{
j = N;
while(j>0) j--;
i--;
}
```

Compute a model (or **intermediate representation**)

Prove termination of the model.

- Hoare rule for total correctness:
- \(\frac{\{t=z \mbox{ and }{t\in D} \mbox{ and } P \mbox { and }B\}S\{P\mbox{ and }t<z\mbox{ and }t\in D\}}{\{\mbox{P}\} \mbox{while B do S done} \{\mbox{not B and P}\}}\)
- with \((D,<)\)
**well founded**

- In our case:
- \(D=(\mathbb{N}^d,<_{lex})\) and
- we look for \(\rho(k,-)\) positive and
**strictly**decreasing. - we need (numerical)
**invariants**\({\cal I}_k\)!

From the program representation, we build a system of constraints:

- \(\rho\) is positive : \(\rho(k,\vec{x})\geq 0\) on \({\cal I}_{k}\)
- \(\rho\) is decreasing : \(\vec{x'}-\vec{x^{}}\in \tau \Rightarrow \rho(dest,\vec{x'})-\rho(src,\vec{x^{}})<0\)

We transform it into a Linear Programming instance

We solve.

Rank tool on compsys-tools.ens-lyon.fr

- applicability: only numerical programs
- abstraction of all non-numerical statements
- not enough!

- scalability:
- complexity is \(O(nbvars*nbcontrolpoints*dim)\)
- LP instances are too big
- using slicing is not enough

- [WST14] (with F. Pereira, Brasil):
**realworld**loops are simple !- slice and pattern-match

- [Submitted to PLDI] (with D. Monniaux, Grenoble) : only a few assignments in a loop actually matter !
- Consider loops as
**single transitions**and only**heads of loops** - Compute incrementally the LP-problem.

- Consider loops as

- Improvement of the state of the art thanks to methods coming from:
- Polyhedral scheduling (Feautrier)
- Static analysis (Abstract interpretation, \(\ldots\))
- Logic : SMT solvers, optimising SMT solvers

- Future work:
- scalability : consolidate Termite's implementation. (D. Monniaux, G. Radanne)
- applicability : look at
**rewriting techniques**for termination of recursive functions, or complex data structures (C. Fuhs, Plume)