Virgile Prevosto

ORCID

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 29

Top Venues

Pierre and Marie Curie University, Paris, France (PHD)

Education History

Pierre and Marie Curie University, Paris, France

PHD

Publications

Louis Gauthier, Virgile Prevosto, Julien Signoles
A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification. FormaliSE@ICSE (2024)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
An Efficient VCGen-based Modular Verification of Relational Properties. CoRR (2024)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
Certified Verification of Relational Properties. IFM (2022)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
An Efficient VCGen-Based Modular Verification of Relational Properties. ISoLA (1) (2022)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
Certified Verification of Relational Properties. CoRR (2022)
Thibault Martin, Nikolai Kosmatov, Virgile Prevosto
Verifying redundant-check based countermeasures: a case study. SAC (2022)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
Methodology for Specification and Verification of High-Level Requirements with MetAcsl. FormaliSE@ICSE (2021)
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
The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64 (8) (2021)
Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre
Detection of Polluting Test Objectives for Dataflow Criteria. IFM (2020)
Catherine Dubois, Virgile Prevosto, Guillaume Burel
Teaching Formal Methods to Future Engineers. FMTea (2019)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. TAP@FM (2019)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
MetAcsl: Specification and Verification of High-Level Properties. TACAS (1) (2019)
Steven de Oliveira, Virgile Prevosto, Peter Habermehl, Saddek Bensalem
Left-Eigenvectors Are Certificates of the Orbit Problem. RP (2018)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
Self-composition to Prove Relational Properties in Annotated C Program. CoRR (2018)
Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson
Time to clean your test objectives. ICSE (2018)
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
MetAcsl: Specification and Verification of High-Level Properties. CoRR (2018)
Steven de Oliveira, Virgile Prevosto, Peter Habermehl, Saddek Bensalem
Left-eigenvectors are certificates of the Orbit Problem. CoRR (2018)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot
Static and Dynamic Verification of Relational Properties on Self-composed C Code. TAP@STAF (2018)
Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson
Freeing Testers from Polluting Test Objectives. CoRR (2017)
Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
Synthesizing Invariants by Solving Solvable Loops. ATVA (2017)
Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto
Symbolic Execution of Transition Systems with Function Summaries. TAP@STAF (2017)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
RPP: Automatic Proof of Relational Properties by Self-composition. TACAS (1) (2017)
Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Virgile Prevosto
Taming Coverage Criteria Heterogeneity with LTest. ICST (2017)
Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov, Virgile Prevosto
Generic and Effective Specification of Structural Test Objectives. ICST (2017)
Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Michaël Marcozzi, Virgile Prevosto
Generic and Effective Specification of Structural Test Objectives. CoRR (2016)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
Deductive Verification with Relational Properties. CoRR (2016)
Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
Polynomial invariants by linear algebra. CoRR (2016)
Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
Synthesizing invariants by solving solvable loops. CoRR (2016)
Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
Polynomial Invariants by Linear Algebra. ATVA (2016)
Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
Frama-C: A software analysis perspective. Formal Aspects Comput. 27 (3) (2015)
Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto
Model-Based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts. ICTSS (2015)
Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper. TAP@STAF (2013)
Virgile Prevosto, Jochen Burghardt, Jens Gerlach, Kerstin Hartig, Hans Werner Pohl, Kim Völlinger
Formal specification and automated verification of railway software with Frama-C. INDIN (2013)
Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
Frama-C - A Software Analysis Perspective. SEFM (2012)
Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski, Xuejun Yang
Testing Static Analyzers with Randomly Generated Programs. NASA Formal Methods (2012)
Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto
Functional dependencies of C functions via weakest pre-conditions. Int. J. Softw. Tools Technol. Transf. 13 (5) (2011)
Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon, Géraud Canet, Loïc Correnson, Benjamin Monate, Virgile Prevosto, Armand Puccetti
Experience report: OCaml for an industrial-strength static analysis framework. ICFP (2009)
Virgile Prevosto, Sylvain Boulmé
Proof Contexts with Late Binding. TLCA (2005)
Virgile Prevosto
Certified mathematical hierarchies: the FoCal system. Mathematics, Algorithms, Proofs (2005)
David Delahaye, Mathieu Jaume, Virgile Prevosto
Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs. Tech. Sci. Informatiques 24 (9) (2005)
Virgile Prevosto, Damien Doligez, Thérèse Hardin
Algebraic Structures and Dependent Records. TPHOLs (2002)
Virgile Prevosto, Damien Doligez
Algorithms and Proofs Inheritancey in the FOC Language. J. Autom. Reason. 29 (3-4) (2002)
Virgile Prevosto
Prototype d'interface utilisateur de la librairie FOC. JFLA (2001)

Virgile Prevosto.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Virgile Prevosto