Virgile Prevosto

According to our database, Virgile Prevosto authored at least 38 papers between 2001 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

High-Level Program Properties in Frama-C: Definition, Verification and Deduction.

Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification, 2024

A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification.

Louis Gauthier, Virgile Prevosto, Julien Signoles

Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), 2024

2022

Verifying redundant-check based countermeasures: a case study.

Thibault Martin, Nikolai Kosmatov, Virgile Prevosto

Proceedings of the SAC '22: The 37th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, April 25, 2022

An Efficient VCGen-Based Modular Verification of Relational Properties.

Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

Certified Verification of Relational Properties.

Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall

Proceedings of the Integrated Formal Methods - 17th International Conference, 2022

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

Methodology for Specification and Verification of High-Level Requirements with MetAcsl.

Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall

Proceedings of the 9th IEEE/ACM International Conference on Formal Methods in Software Engineering, 2021

2020

Detection of Polluting Test Objectives for Dataflow Criteria.

Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre

Proceedings of the Integrated Formal Methods - 16th International Conference, 2020

2019

Teaching Formal Methods to Future Engineers.

Catherine Dubois, Virgile Prevosto, Guillaume Burel

Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties.

Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall

Proceedings of the Tests and Proofs - 13th International Conference, 2019

MetAcsl: Specification and Verification of High-Level Properties.

Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

2018

Self-composition to Prove Relational Properties in Annotated C Program.

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto

CoRR, 2018

Static and Dynamic Verification of Relational Properties on Self-composed C Code.

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot

Proceedings of the Tests and Proofs - 12th International Conference, 2018

Left-Eigenvectors Are Certificates of the Orbit Problem.

Steven de Oliveira, Virgile Prevosto, Peter Habermehl, Saddek Bensalem

Proceedings of the Reachability Problems - 12th International Conference, 2018

Time to clean your test objectives.

Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson

Proceedings of the 40th International Conference on Software Engineering, 2018

2017

Freeing Testers from Polluting Test Objectives.

Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loïc Correnson

CoRR, 2017

Symbolic Execution of Transition Systems with Function Summaries.

Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto

Proceedings of the Tests and Proofs - 11th International Conference, 2017

RPP: Automatic Proof of Relational Properties by Self-composition.

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Generic and Effective Specification of Structural Test Objectives.

Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov, Virgile Prevosto

Proceedings of the 2017 IEEE International Conference on Software Testing, 2017

Taming Coverage Criteria Heterogeneity with LTest.

Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Virgile Prevosto

Proceedings of the 2017 IEEE International Conference on Software Testing, 2017

Synthesizing Invariants by Solving Solvable Loops.

Steven de Oliveira, Saddek Bensalem, Virgile Prevosto

Proceedings of the Automated Technology for Verification and Analysis, 2017

2016

Deductive Verification with Relational Properties.

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto

CoRR, 2016

Polynomial Invariants by Linear Algebra.

Steven de Oliveira, Saddek Bensalem, Virgile Prevosto

Proceedings of the Automated Technology for Verification and Analysis, 2016

2015

Frama-C: A software analysis perspective.

Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski

Formal Aspects Comput., 2015

Model-Based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts.

Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto

Proceedings of the Testing Software and Systems, 2015

2013

A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper.

Nikolai Kosmatov, Virgile Prevosto, Julien Signoles

Proceedings of the Tests and Proofs - 7th International Conference, 2013

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

Proceedings of the 11th IEEE International Conference on Industrial Informatics, 2013

2012

Frama-C - A Software Analysis Perspective.

Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski

Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

Testing Static Analyzers with Randomly Generated Programs.

Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski, Xuejun Yang

Proceedings of the NASA Formal Methods, 2012

2011

Functional dependencies of C functions via weakest pre-conditions.

Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto

Int. J. Softw. Tools Technol. Transf., 2011

2009

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

Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

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

Proof Contexts with Late Binding.

Virgile Prevosto, Sylvain Boulmé

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Certified mathematical hierarchies: the FoCal system.

Virgile Prevosto

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

2003

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

PhD thesis, 2003

2002

Algorithms and Proofs Inheritancey in the FOC Language.

Virgile Prevosto, Damien Doligez

J. Autom. Reason., 2002

Algebraic Structures and Dependent Records.

Virgile Prevosto, Damien Doligez, Thérèse Hardin

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

2001

Prototype d'interface utilisateur de la librairie FOC.

Virgile Prevosto

Proceedings of the Journées francophones des langages applicatifs (JFLA'01), 2001