Search

Your search keyword '"Prevosto, Virgile"' showing total 96 results
Start Over Author "Prevosto, Virgile"

Refine your results

more »

more »

more »

more »
96 results on '"Prevosto, Virgile"'

53. A Component-Based Formal Language Workbench

Author

Mosses, P.D., Monahan, Rosemary, Prevosto, Virgile, and Proença, José

Subjects
FOS: Computer and information sciences, formal semantics, Exploit, Computer science, IDE, Formal semantics (linguistics), Short paper, computer.software_genre, lcsh:QA75.5-76.95, components, Computer Science - Software Engineering, D.2.13, programming languages, Formal language, Formal description, language workbench, D.3.1, Computer Science - Programming Languages, Programming language, lcsh:Mathematics, D.2.6, Work in process, lcsh:QA1-939, Software Engineering (cs.SE), F.3.2, Programming language specification, Workbench, lcsh:Electronic computers. Computer science, computer, Programming Languages (cs.PL)
Abstract

The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications. After introducing CBS and its formal definition, this short paper reports work in progress on generating an IDE for CBS from the definition. It also considers the possibility of supporting component-based language specification in other formal language workbenches., Comment: In Proceedings F-IDE 2019, arXiv:1912.09611

Published
2019
Full Text
View/download PDF

54. Time to Clean Your Test Objectives

Author

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

Published
2018

56. Time to clean your test objectives

Author

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

Published
2018
Full Text
View/download PDF

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

Author

Vedrine Franck, Marteau Helene, Sadmi Franck, Prevosto Virgile, Duboc Lucas, Kirchner Florent, Flanc Sebastien, Bureau Veritas, Bureau Veritas Marine & Offshore, SIREHNA, SIREHNA Atlantic, Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Boyer, Marc, and Laboratoire d'Intégration des Systèmes et des Technologies (LIST)

Subjects
Engineering, business.industry, Software development, System testing, Context (language use), Safety standards, [INFO.INFO-ES] Computer Science [cs]/Embedded Systems, Software, SAFER, Systems engineering, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Software system, business, Formal verification
Abstract

As the development of ship software systems has followed the growth curve of digital technologies, Marine & Offshore assessors like BUREAU VERITAS, are lacking dedicated software standards and tools which are available to other industrial sectors like railways or aeronautics. Indeed, in this field of Marine & Offshore, software systems are seen as black-boxes, i.e. only verified through system testing with minimal requirements specific to software development. Given the potential effect impact of software failures on human, strategic, economic, and/or environmental aspects, the current approach is inadequate. As a result of this, BUREAU VERITAS has developed pragmatic guideline for the development and assessment of marine & offshore verification software which meet the rigorous safety standards required for this industry. These guidelines focus on development processes and the use of efficient tools to verify software through a white-box approach. In this context BUREAU VERITAS has partnered with CEA-LIST who is industry leader in applied formal verification techniques. This paper is supplemented by a project case study where these guidelines have been applied to the review of a critical ship software system owned by SIREHNA (a subsidiary of DCNS).

Published
2016

60. Certified mathematical hierarchies: the FoCal system

Author

Prevosto, Virgile

Subjects
Focal, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, proofs, inheritance, Coq, refinement, types, computer algebra, Specifications
Abstract

The focal language (formerly Foc) allows a programmer to incrementally build mathematical structures and to formally prove their correctness. focal encourages a development process by refinement, deriving step-by-step implementations from specifications. This refinement process is realized using an inheritance mechanism on structures which can mix primitive operations, axioms, algorithms and proofs. Inheritance from existing structures allows to reuse their components under some conditions, which are statically checked by the compiler. In this talk, we first present the main constructions of the language. Then we show a shallow embedding of these constructions in the Coq proof assistant, which is used to check the proofs made in Focal. Such a proof can be either an hand-written Coq script, made in an environment set up by the Focal compiler, or a Coq term given the zenon theorem prover, which is partly developped within Focal. Last, we present a formalization of focal structures and show that the Coq embedding is conform to this model.

Published
2006
Full Text
View/download PDF

62. Certified mathematical hierarchies: the FoCal system

Author

Virgile Prevosto, Prevosto, Virgile, Virgile Prevosto, and Prevosto, Virgile

Abstract

The focal language (formerly Foc) allows a programmer to incrementally build mathematical structures and to formally prove their correctness. focal encourages a development process by refinement, deriving step-by-step implementations from specifications. This refinement process is realized using an inheritance mechanism on structures which can mix primitive operations, axioms, algorithms and proofs. Inheritance from existing structures allows to reuse their components under some conditions, which are statically checked by the compiler. In this talk, we first present the main constructions of the language. Then we show a shallow embedding of these constructions in the Coq proof assistant, which is used to check the proofs made in Focal. Such a proof can be either an hand-written Coq script, made in an environment set up by the Focal compiler, or a Coq term given the zenon theorem prover, which is partly developped within Focal. Last, we present a formalization of focal structures and show that the Coq embedding is conform to this model.

Published
2006
Full Text
View/download PDF

63. Experience report

Author

Cuoq, Pascal, primary, Signoles, Julien, additional, Baudin, Patrick, additional, Bonichon, Richard, additional, Canet, Géraud, additional, Correnson, Loïc, additional, Monate, Benjamin, additional, Prevosto, Virgile, additional, and Puccetti, Armand, additional

Published
2009
Full Text
View/download PDF

65. Frama-C.

Author

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

Published
2012
Full Text
View/download PDF

66. Experience report.

Author

Cuoq, Pascal, Signoles, Julien, Baudin, Patrick, Bonichon, Richard, Canet, Géraud, Correnson, Loïc, Monate, Benjamin, Prevosto, Virgile, and Puccetti, Armand

Published
2009
Full Text
View/download PDF

67. Proof Contexts with Late Binding.

Author

Urzyczyn, Paweł, Prevosto, Virgile, and Boulmé, Sylvain

Abstract

The Focal language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for encoding Focal constructions in the Coq proof assistant. The first one is implemented in the Focal compiler to have the correctness of Focal libraries verified with the Coq proof-checker. The second one formalizes the Focal structures and their main properties as Coq terms (called mixDrecs). The relations between the two embeddings are examined in the last part of the paper. [ABSTRACT FROM AUTHOR]

Published
2005
Full Text
View/download PDF

70. An Exercise in Mind Reading: Automatic Contract Inference for Frama-C

Author

Amilon, Jesper, Esen, Zafer, Gurov, Dilian, Lidström, Christian, Rümmer, Philipp, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

71. Proof of Security Properties: Application to JavaCard Virtual Machine

Author

Djoudi, Adel, Hána, Martin, Kosmatov, Nikolai, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

72. Ten Years of Industrial Experiments with Frama-C at Mitsubishi Electric R&D Centre Europe

Author

Lavillonnière, Éric, Mentré, David, Boyer, Benoît, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

73. Exploring Frama-C Resources by Verifying Space Software

Author

Busquim e Silva, Rovedy Aparecida, Arai, Nanci Naomi, Burgareli, Luciana Akemi, Parente de Oliveira, Jose Maria, Sousa Pinto, Jorge, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

74. Combining Analyses Within Frama-C

Author

Kosmatov, Nikolai, Plaunov, Artjom, Shankar, Subash, Signoles, Julien, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

75. Analysis of Embedded Numerical Programs in the Presence of Numerical Filters

Author

Védrine, Franck, Piriou, Pierre-Yves, David, Vincent, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

76. Advanced Memory and Shape Analyses

Author

Lemerre, Matthieu, Rival, Xavier, Nicole, Olivier, Illous, Hugo, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

77. Tools for Program Understanding

Author

Maroneze, André, Perrelle, Valentin, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

78. Test Generation with PathCrawler PathCrawler (Frama-C plug-in)

Author

Williams, Nicky, Kosmatov, Nikolai, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

79. Formally Verifying that a Program Does What It Should: The Wp Wp (Frama-C plug-in) Plug-in

Author

Blanchard, Allan, Bobot, François, Baudin, Patrick, Correnson, Loïc, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

80. Runtime Annotation Checking with Frama-C: The E-ACSL E-ACSL (Frama-C plug-in) Plug-in

Author

Benjamin, Thibaut, Signoles, Julien, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

81. Abstract Interpretation with the Eva Eva (Frama-C plug-in) Plug-in

Author

Bühler, David, Maroneze, André, Perrelle, Valentin, Abraham, Erika, Editorial Board Member, Beyersdorff, Olaf, Editorial Board Member, Blanchette, Jasmin, Editorial Board Member, Biere, Armin, Editorial Board Member, Buss, Sam, Editorial Board Member, England, Matthew, Editorial Board Member, Fleuriot, Jacques, Editorial Board Member, Fontaine, Pascal, Editorial Board Member, Gurfinkel, Arie, Editorial Board Member, Heule, Marijn, Editorial Board Member, Kahle, Reinhard, Editorial Board Member, Kolaitis, Phokion, Editorial Board Member, Kolokolova, Antonina, Editorial Board Member, Matthes, Ralph, Editorial Board Member, Mahboubi, Assia, Editorial Board Member, Nordström, Jakob, Editorial Board Member, Panangaden, Prakash, Editorial Board Member, Rozier, Kristin Yvonne, Editorial Board Member, Studer, Thomas, Editorial Board Member, Tinelli, Cesare, Editorial Board Member, Kosmatov, Nikolai, editor, Prevosto, Virgile, editor, and Signoles, Julien, editor

Published
2024
Full Text
View/download PDF

82. Testing a Formally Verified Compiler

Author

Monniaux, David, Gourdin, Léo, Boulmé, Sylvain, Lebeltel, Olivier, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Prevosto, Virgile, editor, and Seceleanu, Cristina, editor

Published
2023
Full Text
View/download PDF

83. Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars

Author

Strauss, Megan, Mitsch, Stefan, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Prevosto, Virgile, editor, and Seceleanu, Cristina, editor

Published
2023
Full Text
View/download PDF

85. Testing Languages with a Languages-as-Databases Approach

Author

Cimini, Matteo, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Prevosto, Virgile, editor, and Seceleanu, Cristina, editor

Published
2023
Full Text
View/download PDF

87. Symbolic Observation Graph-Based Generation of Test Paths

Author

Klai, Kais, Bennani, Mohamed Taha, Arias, Jaime, Desel, Jörg, Ochi, Hanen, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Prevosto, Virgile, editor, and Seceleanu, Cristina, editor

Published
2023
Full Text
View/download PDF

88. Low-Level Reachability Analysis Based on Formal Logic

Author

Naus, Nico, Verbeek, Freek, Schoolderman, Marc, Ravindran, Binoy, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Prevosto, Virgile, editor, and Seceleanu, Cristina, editor

Published
2023
Full Text
View/download PDF

91. Proving Properties of Operation Contracts with Test Scenarios

Author

Gogolla, Martin, Hamann, Lars, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Prevosto, Virgile, editor, and Seceleanu, Cristina, editor

Published
2023
Full Text
View/download PDF

92. An efficient VCGen-based modular verification of relational properties

Author

Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall, Karlsruhe Institute of Technology (KIT), Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Thales Research and Technology [Palaiseau], THALES [France], Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Laboratoire Sûreté des Logiciels (LSL), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), CentraleSupélec, Mathématiques et Informatique pour la Complexité et les Systèmes (MICS), CentraleSupélec-Université Paris-Saclay, and Prevosto, Virgile

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
Abstract

International audience; Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Relational properties link several function calls together within a single specification. They can express more advanced properties of a given function or relate calls to different functions, possibly run in parallel. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Recent work proposed a new technique for relational property verification that relies on a verification condition generator to produce logical formulas that must be verified to ensure a given relational property. This paper presents an overview of this approach and proposes important enhancements. We integrate an optimized verification condition generator and extend the underlying theory to show how relational properties can be proved in a modular way, where one relational property can be used to prove another one, like in modular verification of function contracts. Our results have been fully formalized and proved sound in the Coq proof assistant.

Published
2022

93. Lightweight Interactive Proving inside an Automatic Program Verifier

Author

Sylvain Dailler, Yannick Moy, Claude Marché, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), AdaCore (FRANCE), Masci, Paolo, Monahan, Rosemary, and Prevosto, Virgile

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer science, 02 engineering and technology, computer.software_genre, lcsh:QA75.5-76.95, Toolchain, Computer Science - Software Engineering, Software, 020204 information systems, Formal specification, 0202 electrical engineering, electronic engineering, information engineering, Code (cryptography), computer.programming_language, Computer Science - Programming Languages, SIMPLE (military communications protocol), business.industry, Programming language, lcsh:Mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, lcsh:QA1-939, Formal methods, Logic in Computer Science (cs.LO), Software Engineering (cs.SE), SPARK (programming language), TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, lcsh:Electronic computers. Computer science, User interface, business, computer, Programming Languages (cs.PL)
Abstract

Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts. In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the-art automatic provers. Adding interactive proof features in SPARK appears to be complicated by the fact that the proof toolchain makes use of the independent, intermediate verification tool Why3, which is generic enough to accept multiple front-ends for different input languages. This paper reports on our approach to extend Why3 with interactive proof features and also with a generic client-server infrastructure allowing integration of proof interaction into an external, front-end graphical user interface such as the one of SPARK., In Proceedings F-IDE 2018, arXiv:1811.09014

Published
2018

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

Author

Prévosto, Virgile, Védrine, Franck, Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), and Prevosto, Virgile

Subjects
[INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], ComputingMilieux_MISCELLANEOUS
Abstract

International audience

Published
2014

95. Formal specification and automated verification of railway software with Frama-C

Author

Kim Voellinger, Kerstin Hartig, Hans Pohl, Jochen Burghardt, Virgile Prevosto, Jens Gerlach, Prevosto, Virgile, CARN - - DEVICE SOFT2009 - ANR-09-CARN-0006 - CARN - VALID, Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Fraunhofer Institute for Open Communication Systems (Fraunhofer FOKUS), Fraunhofer (Fraunhofer-Gesellschaft), ANR-09-CARN-0006,DEVICE SOFT(2009), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), and Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
business.industry, Computer science, [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], 020207 software engineering, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 02 engineering and technology, Formal methods, Intelligent verification, 020204 information systems, Formal specification, Software construction, 0202 electrical engineering, electronic engineering, information engineering, Verification, Software verification and validation, Software engineering, business, Formal verification, Software verification
Abstract

International audience; —This paper presents the use of the Frama-C toolkit for the formal verification of a model of train-controlling software against the requirements of the CENELEC norm EN 50128. We also compare our formal approach with traditional unit testing.

Published
2013

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

Author

Prévosto, Virgile, Sémantiques, preuves et implantation (SPI), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Université Pierre et Marie Curie - Paris VI, Hardin Thérèse, Doligez Damien, and Prevosto, Virgile

Subjects
langages de programmation, vérification de logiciel, programmation fonctionnelle, programming languages, type theory, [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], software verification, functional programming, object-oriented programming, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], théorie des types, programmation orientée-objet
Abstract

This thesis describes the construction of an environment to develop certified computer algebra libraries. First, we present species, the structures used to describe specifications, by multiple inheritance, refinement and parameterization. Collections are built by encapsulation of species and form the user library. We also define the static analyses that guarantee the correction of a species definition. Then, we study the compilation of species and collections into the programming language OCAML, with the use of OCAML's objects and modules. After that, we detail the translation into the proof language COQ, the late binding being translated by lambda-abstractions. We then show how this technique can be used to optimise OCAML executables. Last, we prove that the analyses performed by the compiler, as well as the translation mechanisms are correct with respect to the species formalisation made previously in COQ., Cette thèse porte sur la construction d'un environnement pour développer des librairies de calcul formel certifié. Nous présentons d'abord les espèces, structures servant à décrire des spécifications par héritage multiple, raffinement et paramétrisation. Les collections, construites par encapsulation d'espèces constituent la librairie utilisateur. Nous définissons également les analyses statiques garantissant la correction d'une définition d'espèce. Ensuite, nous étudions la compilation des espèces et collections vers le langage d'exécution OCAML, en utilisant les objets et modules OCAML. Puis nous détaillons la traduction dans le langage de preuves COQ, la liaison retardée étant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les exécutables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme à la formalisation des espèces faites auparavant en COQ.

Published
2003

Catalog

Books, media, physical & digital resources
See catalog results