Virgile Prevosto

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