Prototype d'interface utilisateur de la librairie FOC. - Virgile Prevosto (JFLA, 2001)

Algebraic Structures and Dependent Records. - Virgile Prevosto; Damien Doligez; Thérèse Hardin (TPHOLs, 2002)

Algorithms and Proofs Inheritancey in the FOC Language. - Virgile Prevosto; Damien Doligez (J. Autom. Reason., 2002)

Conception et implantation du langage FoC pour le développement de logiciels certifiés. (Design and implementation of the FoC language for developping certified software). - Virgile Prevosto (2003)

Certified mathematical hierarchies: the FoCal system. - Virgile Prevosto (Mathematics, Algorithms, Proofs, 2005)

Proof Contexts with Late Binding. - Virgile Prevosto; Sylvain Boulmé (TLCA, 2005)

Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs. - David Delahaye; Mathieu Jaume; Virgile Prevosto (Tech. Sci. Informatiques, 2005)

Experience report: OCaml for an industrial-strength static analysis framework. - Pascal Cuoq; Julien Signoles; Patrick Baudin; Richard Bonichon; Géraud Canet; Loïc Correnson; Benjamin Monate; Virgile Prevosto; Armand Puccetti (ICFP, 2009)

Functional dependencies of C functions via weakest pre-conditions. - Pascal Cuoq; Benjamin Monate; Anne Pacalet; Virgile Prevosto (Int. J. Softw. Tools Technol. Transf., 2011)

Testing Static Analyzers with Randomly Generated Programs. - Pascal Cuoq; Benjamin Monate; Anne Pacalet; Virgile Prevosto; John Regehr; Boris Yakobowski; Xuejun Yang (NASA Formal Methods, 2012)

Frama-C - A Software Analysis Perspective. - Pascal Cuoq; Florent Kirchner; Nikolai Kosmatov; Virgile Prevosto; Julien Signoles; Boris Yakobowski (SEFM, 2012)

Formal specification and automated verification of railway software with Frama-C. - Virgile Prevosto; Jochen Burghardt; Jens Gerlach; Kerstin Hartig; Hans Werner Pohl; Kim Völlinger (INDIN, 2013)

A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper. - Nikolai Kosmatov; Virgile Prevosto; Julien Signoles (TAP@STAF, 2013)

Model-Based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts. - Imen Boudhiba; Christophe Gaston; Pascale Le Gall; Virgile Prevosto (ICTSS, 2015)

Frama-C: A software analysis perspective. - Florent Kirchner; Nikolai Kosmatov; Virgile Prevosto; Julien Signoles; Boris Yakobowski (Formal Aspects Comput., 2015)

Polynomial Invariants by Linear Algebra. - Steven de Oliveira; Saddek Bensalem; Virgile Prevosto (ATVA, 2016)

Deductive Verification with Relational Properties. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto (CoRR, 2016)

Synthesizing Invariants by Solving Solvable Loops. - Steven de Oliveira; Saddek Bensalem; Virgile Prevosto (ATVA, 2017)

Taming Coverage Criteria Heterogeneity with LTest. - Michaël Marcozzi; Sébastien Bardin; Mickaël Delahaye; Nikolai Kosmatov; Virgile Prevosto (ICST, 2017)

Generic and Effective Specification of Structural Test Objectives. - Michaël Marcozzi; Mickaël Delahaye; Sébastien Bardin; Nikolai Kosmatov; Virgile Prevosto (ICST, 2017)

RPP: Automatic Proof of Relational Properties by Self-composition. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto (TACAS (1), 2017)

Symbolic Execution of Transition Systems with Function Summaries. - Imen Boudhiba; Christophe Gaston; Pascale Le Gall; Virgile Prevosto (TAP@STAF, 2017)

Freeing Testers from Polluting Test Objectives. - Michaël Marcozzi; Sébastien Bardin; Nikolai Kosmatov; Mike Papadakis; Virgile Prevosto; Loïc Correnson (CoRR, 2017)

Time to clean your test objectives. - Michaël Marcozzi; Sébastien Bardin; Nikolai Kosmatov; Mike Papadakis; Virgile Prevosto; Loïc Correnson (ICSE, 2018)

Left-Eigenvectors Are Certificates of the Orbit Problem. - Steven de Oliveira; Virgile Prevosto; Peter Habermehl; Saddek Bensalem (RP, 2018)

Static and Dynamic Verification of Relational Properties on Self-composed C Code. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto; Guillaume Petiot (TAP@STAF, 2018)

Self-composition to Prove Relational Properties in Annotated C Program. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto (CoRR, 2018)

MetAcsl: Specification and Verification of High-Level Properties. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Louis Rilling; Pascale Le Gall (TACAS (1), 2019)

Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Louis Rilling; Pascale Le Gall (TAP@FM, 2019)

Teaching Formal Methods to Future Engineers. - Catherine Dubois; Virgile Prevosto; Guillaume Burel (FMTea, 2019)

Detection of Polluting Test Objectives for Dataflow Criteria. - Thibault Martin; Nikolai Kosmatov; Virgile Prevosto; Matthieu Lemerre (IFM, 2020)

Methodology for Specification and Verification of High-Level Requirements with MetAcsl. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Louis Rilling; Pascale Le Gall (FormaliSE@ICSE, 2021)

The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. - Patrick Baudin; François Bobot; David Bühler; Loïc Correnson; Florent Kirchner; Nikolai Kosmatov; André Maroneze; Valentin Perrelle; Virgile Prevosto; Julien Signoles; Nicky Williams (Commun. ACM, 2021)

Certified Verification of Relational Properties. - Lionel Blatter; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall (IFM, 2022)

An Efficient VCGen-Based Modular Verification of Relational Properties. - Lionel Blatter; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall (ISoLA (1), 2022)

Verifying redundant-check based countermeasures: a case study. - Thibault Martin; Nikolai Kosmatov; Virgile Prevosto (SAC, 2022)

A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification. - Louis Gauthier; Virgile Prevosto; Julien Signoles (FormaliSE@ICSE, 2024)

High-Level Program Properties in Frama-C: Definition, Verification and Deduction. - Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall (ISoLA (3), 2024)

Typestates Specification and Verification in Frama-C. - Sébastien Patte; Virgile Prevosto (FormaliSE, 2025)