Skip to content

Virgile Prevosto

Publication record assembled from the DBLP archive of ranked conferences.

Papers indexed

21

Venues

11

Active years

2009–2025

Best venue rank

A*

Where they publish

Papers

21 indexed papers, newest first.

YearVenueTitleAuthors
2025IFMFormal Verification of PKCS#1 Signature Parser Using Frama-C.Martin Hna, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
2024ISoLAHigh-Level Program Properties in Frama-C: Definition, Verification and Deduction.Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022IFMCertified Verification of Relational Properties.Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022ISoLAAn Efficient VCGen-Based Modular Verification of Relational Properties.Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022SACVerifying redundant-check based countermeasures: a case study.Thibault Martin, Nikolai Kosmatov, Virgile Prevosto
2021ICSEMethodology for Specification and Verification of High-Level Requirements with MetAcsl.Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
2020IFMDetection of Polluting Test Objectives for Dataflow Criteria.Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre
2019TACASMetAcsl: Specification and Verification of High-Level Properties.Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
2019TAPTame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties.Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
2018ICSETime to clean your test objectives.Michal Marcozzi, Sbastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto, Loc Correnson
2018TAPStatic and Dynamic Verification of Relational Properties on Self-composed C Code.Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot
2017ATVASynthesizing Invariants by Solving Solvable Loops.Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
2017ICSTTaming Coverage Criteria Heterogeneity with LTest.Michal Marcozzi, Sbastien Bardin, Mickal Delahaye, Nikolai Kosmatov, Virgile Prevosto
2017ICSTGeneric and Effective Specification of Structural Test Objectives.Michal Marcozzi, Mickal Delahaye, Sbastien Bardin, Nikolai Kosmatov, Virgile Prevosto
2017TACASRPP: Automatic Proof of Relational Properties by Self-composition.Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
2017TAPSymbolic Execution of Transition Systems with Function Summaries.Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto
2016ATVAPolynomial Invariants by Linear Algebra.Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
2013INDINFormal specification and automated verification of railway software with Frama-C.Virgile Prevosto, Jochen Burghardt, Jens Gerlach, Kerstin Hartig, Hans Werner Pohl, Kim Vllinger
2013TAPA Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper.Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
2012SEFMFrama-C - A Software Analysis Perspective.Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
2009ICFPExperience report: OCaml for an industrial-strength static analysis framework.Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon, Graud Canet, Loc Correnson, Benjamin Monate, Virgile Prevosto, Armand Puccetti