Publications

2018

1. De Oliveira Steven, Prevosto Virgile, Peter Habermehl and Bensalem Saddek (RP 2018)
   Left-eigenvectors are certificates of the Orbit Problem
   

   This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we reduce the problem of generating linear and polynomial certificates of non-reachability for the Orbit Problem for linear transformations with rational coefficients to the generalized eigenvector problem. Also, we prove the existence of such certificates for any transformation with integer coefficients, which is not the case with rational coefficients.

2. De Oliveira Steven (Manuscript)
   Finding constancy in linear routines
   

   This thesis presents new insights on loops containing linear and polynomial instructions. It is already known that linear loops are polynomially expressive, in the sense that if a variable evolves linearly, then any monomial of this variable evolves linearly. The first contribution of this thesis is the extraction of a class of polynomial loops that is exactly as expressive as linear loops, in the sense that there exists a linear loop with the exact same behavior. Then, two new methods for generating invariants are presented. The first method is based on abstract interpretation and is focused on a specific kind of linear loops called linear filters. Linear filters play a role in many embedded systems (plane sensors for example) and require the use of floating point operations, that may be imprecise and lead to errors if they are badly handled. Also, the presence of non deterministic assignments makes their analysis even more complex. The second method treats of a more generic subject by finding a complete set of linear invariants of linear loops that is easily computable. This technique is based on the linear algebra concept of eigenspace. It is extended to deal with conditions, nested loops and non determinism in assignments. Generating invariants is an interesting topic, but it is not an end in itself, it must serve a purpose. This thesis investigates the expressivity of invariants generated by the second method by generating counter examples for the Kannan-Lipton Orbit problem. It also presents the tool PILAT implementing this technique and compares its efficiency technique with other state-of-the-art invariant synthesizers. The effective usefulness of the invariants generated by PILAT is demonstrated by using the tool in concert with CaFE, a model-checker for C programs based on temporal logics.

2017

3. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2017, October)
   Synthesizing invariants by solving solvable loops
   In 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017)

   When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tau-tologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented in the open-source tool Pilat.

4. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2017, June)
   CaFE : un model-checker collaboratif
   In Approches Formelles dans l'Assistance au Developpement Logiciel (AFADL 2017)

   De nombreux travaux s’appuient sur la logique temporelle linéaire (LTL) pour décrire formellement le comportement attendu d’un programme. Une extension particulièrement intéressante de LTL pour l’analyse de programmes est la logique CaRet, qui autorise des raisonnements explicites sur la pile d’appel. Ce papier présente CaFE , un greffon de la plate-forme Frama-C qui vérifie automatiquement de manière approchée qu’un programme C véri- fie une formule logique CaRet donnée. Il décrit également la mise en œuvre de CaFE et ses interactions avec le reste de la plate-forme.

2016

5. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, October)
   Polynomial invariants by linear algebra
   In 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016)

   We present in this paper a new technique for generating polynomial invariants, divided in two independent parts : a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for generating inductive invariants for linear loops. Both of these techniques have a polynomial complexity for a bounded number of variables and we guarantee the completeness of the technique for a bounded degree which we successfully implemented for C programs verification.

6. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, June)
   Algèbre lineaire pour invariant polynomiaux (slides)
   In Approches Formelles dans l'Assistance au Developpement Logiciel (AFADL 2016)

   Nous présentons dans ce papier une nouvelle technique de génération d’invariants dans le contexte d’un certain type de boucles polynomiales. Notre méthode a l’avantage d’être plus rapide que les méthodes existantes pour des boucles équivalentes et plus simple à implanter car elle repose sur des algorithmes d’algèbre linéaire de complexité polynomiale. Un outil implé- mentant cette méthode est en cours de développement dans Frama-C [2], une plateforme open-source, extensible et collaborative dédiée à l’analyse de programmes C.

2015

7. De Oliveira Steven, Prevosto Virgile and Bardin Steven (2015, January).
   Au temps en emporte le C.
   In Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015).

   Le (bon) séquencement des événements au fil du temps fait partie des nombreux sujets d'analyse de programmes, par exemple pour l'étude de protocoles d'échange d'information ou de systèmes embarqués. De nombreux travaux de logique temporelle linéaire (LTL) permettent de décrire formellement le comportement attendu d'un programme, sous la forme d'une succession d’actions distinctes. Implanté au sein de Frama-C, plate-forme d'analyse de code source en langage C, le greffon Aoraï permet la génération de spécifications équivalentes, dans leur ensemble, à la conformité d'un programme C donné vis à vis d'une formule de logique temporelle linéaire. Ce greffon discrétise le temps de telle sorte que seuls les appels et les retours de fonctions sont considérés comme des événements. Cet article présente Model-CaRet, un nouveau greffon Frama-C qui généralise la trace étudiée par Aoraï. Plus précisément, Model-CaRet est dédié à la génération du test de satisfiabilité, et à sa vérification automatique, d'une formule de logique CaRet sur un programme C, représenté sous la forme d'une machine à états récursif. CaRet est une extension naturelle de la LTL permettant l'étude simultanée de plusieurs traces d'exécution, et en particulier de manipuler explicitement la pile d'appel du programme dans les formules.