Steven de Oliveira

Ph.D. Student in formal methods


Since 2014, I work on C programs Model Checking at the Software Safety and Security Laboratory, at the CEA. I mainly work on the development of Frama-C, an open-source framework for the development of C programs verification applications.

  • Development of the model-checker CaFE, based on the temporal logic CaRet
  • Development of the loop invariant generator Pilat, available on GitHub
  • Development of Ocaml libraries of polynomials and matrices (used in Pilat)

You can contact me here. Also, you can find my CV here.

    2016

  1. INF411 - Programmation and algorithms - Ecole Polytechnique
    Jean-Christophe Filliâtre
    • Java
    • Basic data structures (Linked list, trees,...)
    • Genericity

  2. INF431 - Concurrency and distributed computing - Ecole Polytechnique
    Roberto Blanco, Kaustuv Chaudhuri, Steven De Oliveira, Cezara Dragoi, Eric Goubault, Samuel Mimram, Giselle Reis, Christelle Rovetta, Francesco Zappa Nardelli
    • Java
    • Complexity
    • Threads, locks
    • Map-reduce, Hadoop, RMI
  3. Homework : Strange programs and behaviors

    2015

  4. INF472 - Web applications - Ecole Polytechnique
    Steven de Oliveira, Baptiste Desprez, Andrey Ivanov, Christelle Rovetta, Olivier Serre
    • HTML, CSS, PHP
    • Databases (MySQL)
    • Security, javascript, ajax
  5. Open course (in french) : jQuery

    2016

  1. 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.

  2. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, Juin)
    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.

  3. 2015

  4. 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.