Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

45 résultats
Page :
triés par

Taming Coverage Criteria Heterogeneity with LTest

 M. Marcozzi , S. Bardin , M. Delahaye , N. Kosmatov , V. Prevosto
2017 ICST : 10th IEEE International Conference on Software Testing, Verification and Validation, Mar 2017, Tokyo, Japan. pp.500-507, ⟨10.1109/ICST.2017.57⟩
Communication dans un congrès cea-01808788v1

Coq: un outil pour l'enseignement

 David Delahaye , Mathieu Jaume , Virgile Prévosto
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2005, 24, pp.1139-1160
Article dans une revue hal-01125076v1

ANSI/ISO C Specification Language Version 1.20

 Patrick Baudin , Pascal Cuoq , Jean-Christophe Filliâtre , Claude Marché , Benjamin Monate , et al.
CEA List. 2024
Rapport hal-04523865v1
Image document

An efficient VCGen-based modular verification of relational properties

 Lionel Blatter , Nikolai Kosmatov , V. Prevosto , Pascale Le Gall
ISoLA 2022 - 11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2022, Rhodes, Greece
Communication dans un congrès cea-03768250v1
Image document

Generic and Effective Specification of Structural Test Objectives

 Sébastien Bardin , Mickaël Delahaye , Nikolai Kosmatov , Michaël Marcozzi , Virgile Prévosto
2016
Pré-publication, Document de travail cea-01357487v1

Prototype d'interface utilisateur de la librairie Foc

 Virgile Prévosto
JFLA 2001 - 12èmes Journées Francophones des Langages Applicatifs, Jan 2001, Pontarlier, France
Communication dans un congrès hal-01570816v1

RPP: Automatic proof of relational properties by self-composition

 L. Blatter , N. Kosmatov , P. Le Gall , V. Prevosto
TACAS 2017: Tools and Algorithms for the Construction and Analysis of Systems, Apr 2017, Uppsala, Sweden. pp.391-397, ⟨10.1007/978-3-662-54577-5_22⟩
Communication dans un congrès cea-01808885v1
Image document

MetAcsl: Specification and Verification of High-Level Properties

 Virgile Robles , Nikolai Kosmatov , Virgile Prévosto , Louis Rilling , Pascale Le Gall
TACAS 2019, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17462-0_22⟩
Communication dans un congrès cea-02019790v1
Image document

VESSEDIA: Verification Engineering of Safety and Security Critical Industrial Applications Context of the project

 Virgile Prévosto
Rendez-vous de la Recherche et de l'Enseignement en Sécurité des Systèmes d'Information - RESSI, May 2018, La Bresse, France
Communication dans un congrès cea-01835511v1
Image document

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

 Imen Boudhiba , Christophe Gaston , Pascale Le Gall , Virgile Prévosto
Testing Software and Systems , 9447), pp.35-51, 2014, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-25945-1_3⟩
Chapitre d'ouvrage hal-01470156v1

L'atelier Focal

 Catherine Dubois , Mathieu Jaume , Olivier Pons , Virgile Prévosto
AFADL, session outils, Jan 2004, X, France
Communication dans un congrès hal-01125052v1
Image document

Domestiquer la variété des critères de test avec le langage HTOL et l'outil LTest

 Michaël Marcozzi , Sébastien Bardin , Nikolai Kosmatov , Virgile Prévosto , Mickaël Delahaye
Approches Formelles pour l'Assistance au Développement de Logiciels - AFADL, Jun 2017, Montpellier, France
Communication dans un congrès cea-01835544v1
Image document

Safer Marine and Offshore Software with Formal-Verification-Based Guidelines

 Lucas Duboc , Sébastien Flanc , Florent Kirchner , Hélène Marteau , Virgile Prévosto , et al.
8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Jan 2016, TOULOUSE, France
Communication dans un congrès hal-01292258v1
Image document

Symbolic execution of transition systems with function summaries

 Imen Boudhiba , Christophe Gaston , Pascale Le Gall , Virgile Prévosto
11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany
Communication dans un congrès cea-01810693v1

A lesson on proof of programs with Frama-C. Invited tutorial paper

 N. Kosmatov , V. Prevosto , J. Signoles
Tests and Proofs. TAP 2013. Lecture Notes in Computer Science, Jun 2013, Budapest, Hungary. pp.168-177, ⟨10.1007/978-3-642-38916-0_10⟩
Communication dans un congrès istex cea-01834992v1
Image document

CaFE : un model-checker collaboratif

 Steven de Oliveira , Virgile Prévosto , Saddek Bensalem
Approches Formelles pour l'Assistance au Développement du logiciel - AFADL, Jun 2017, Montpellier, France
Communication dans un congrès cea-01835522v1

Coq : un outil pour l'enseignement

 David Delahaye , Mathieu Jaume , Virgile Prévosto
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2005, 24 (9), pp.1139-1160. ⟨10.3166/tsi.24.1139-1160⟩
Article dans une revue istex hal-01195849v1

Symbolic execution of transition systems with function summaries

 I. Boudhiba , C. Gaston , P. Le Gall , V. Prevosto
Lecture Notes in Computer Science, 2017, 10375 LNCS, pp.41-58. ⟨10.1007/978-3-319-61467-0_3⟩
Article dans une revue cea-01808888v1
Image document

projet INGOPCS: Initiative pour la Nouvelle Génération OPC-UA Sécurisée

 Virgile Prévosto , Vincent Monfort , David Maison
Rendez-vous de la Recherche et de l'Enseignement en Sécurité des Systèmes d'Information, May 2017, Grenoble, France
Communication dans un congrès cea-01835563v1
Image document

Formal Specification and Automated Verification of Railway Software with Frama-C

 Virgile Prévosto , Jochen Burghardt , Jens Gerlach , Kerstin Hartig , Hans-Werner Pohl , et al.
IEEE International Conference on Industrial Informatics - INDIN, Jul 2013, Bochum, France
Communication dans un congrès cea-01835639v1

Polynomial invariants by linear algebra

 S. De Oliveira , S. Bensalem , V. Prevosto
Lecture Notes in Computer Science, 2016, 9938 LNCS, pp.479-494. ⟨10.1007/978-3-319-46520-3_30⟩
Article dans une revue cea-01808891v1
Image document

Algèbre linéaire pour invariants polynomiaux

 Steven de Oliveira , Saddek Bensalem , Virgile Prévosto
15èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2016, Besançon, France. pp.61
Communication dans un congrès hal-01391490v1
Image document

Conception et implantation du langage FoC pour le développement de logiciels certifiés

 Virgile Prévosto
Génie logiciel [cs.SE]. Université Pierre et Marie Curie - Paris VI, 2003. Français. ⟨NNT : ⟩
Thèse tel-00007143v1
Image document

Tame your annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties

 Virgile Robles , Nikolai Kosmatov , Virgile Prévosto , Louis Rilling , Pascale Le Gall
International Conference on Tests and Proofs (TAP), Oct 2019, Porto, Portugal. ⟨10.1007/978-3-030-31157-5_11⟩
Communication dans un congrès cea-02301892v1
Image document

Frama-C: A software analysis perspective

 Florent Kirchner , Nikolai Kosmatov , Virgile Prévosto , Julien Signoles , Boris Yakobowski
Formal Aspects of Computing, 2015, 27 (3), pp.573 - 609. ⟨10.1007/s00165-014-0326-7⟩
Article dans une revue cea-01808981v1
Image document

Frama-Clang: a Frama-C front-end for C++

 Virgile Prévosto , Franck Védrine
EuroLLVM, Apr 2014, Edinburgh, United Kingdom
Poster de conférence cea-01835663v1

Algebraic Structures and Dependent Records

 Damien Doligez , Thérèse Hardin , Virgile Prévosto
TPHOLs'02 - 15th International Conference on Theorem Proving in Higher-Order logics, Aug 2002, Hampton, VA, United States. pp.298-313, ⟨10.1007/3-540-45685-6_20⟩
Communication dans un congrès istex hal-01548137v1

The FoC Project: Building a Certified Computer Algebra Library

 Virgile Prévosto
ISSAC 2002 - International Symposium on Symbolic and Algebraic Computation, Jul 2002, Lille, France
Communication dans un congrès hal-01543959v1

FOC, a certified computer algebra library

 Damien Doligez , Thérèse Hardin , Virgile Prévosto
Automath'2002, Apr 2002, Edinburgh, United Kingdom
Communication dans un congrès hal-01544100v1

Formally Expressing what a Program Should Do: the ACSL Language

 Allan Blanchard , Claude Marché , Virgile Prévosto
Nikolai Kosmatov; Julien Signoles. Guide to Software Verification with Frama-C - Core Components, Usages, and Applications, Springer, 2024
Chapitre d'ouvrage hal-04265707v1
Page :