Search

Your search keyword '"Correnson, Loïc"' showing total 32 results
Start Over Author "Correnson, Loïc"
32 results on '"Correnson, Loïc"'

2. 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

3. Automate where Automation Fails: Proof Strategies for Frama-C/WP

Author

Correnson, Loïc, Blanchard, Allan, Djoudi, Adel, Kosmatov, Nikolai, 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, Finkbeiner, Bernd, editor, and Kovács, Laura, editor

Published
2024
Full Text
View/download PDF

5. Ivette: A Modern GUI for Frama-C

Author

Correnson, Loïc, 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, Masci, Paolo, editor, Bernardeschi, Cinzia, editor, Graziani, Pierluigi, editor, Koddenbrock, Mario, editor, and Palmieri, Maurizio, editor

Published
2023
Full Text
View/download PDF

6. Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites

Author

Mussot, Vincent, Zilio, Silvano Dal, Correnson, Loic, Rainjonneau, Serge, Bardout, Yves, and Scano, Grégoire

Subjects
Computer Science - Software Engineering, Computer Science - Logic in Computer Science
Abstract

We propose a new approach for modelling the functional behaviour of an Earth observation satellite. We leverage this approach in order to develop a safety critical software, a "telecommand verifier", that is in charge of checking onboard whether a sequence of instructions is safe for execution. This new service is needed in order to add more autonomy to satellites. To do so, we propose a new Domain Specific Modelling Language and the toolchain required for integration into an embedded software. This framework is based on the composition of deterministic finite state machines with safety conditions , timeouts, and transitions that accept durations as a parameter. It is able to generate code in the synchronous programming language Lustre from a high-level specification of the satellite. This gives a formal way to derive an event-based algorithm simulating the execution of telecommand sequence and, thereupon, a provably correct onboard verifier.

Published
2020

8. Freeing Testers from Polluting Test Objectives

Author

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

Subjects
Computer Science - Software Engineering, D.2.5, D.2.4
Abstract

Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting efficient test suites, able to detect a maximum number of bugs with manageable effort. To do so, they rely on coverage criteria, which define some precise test objectives to be covered. However, many common criteria specify a significant number of objectives that occur to be infeasible or redundant in practice, like covering dead code or semantically equal mutants. Such objectives are well-known to be harmful to the design of test suites, impacting both the efficiency and precision of testers' effort. This work introduces a sound and scalable formal technique able to prune out a significant part of the infeasible and redundant objectives produced by a large panel of white-box criteria. In a nutshell, we reduce this challenging problem to proving the validity of logical assertions in the code under test. This technique is implemented in a tool that relies on weakest-precondition calculus and SMT solving for proving the assertions. The tool is built on top of the Frama-C verification platform, which we carefully tune for our specific scalability needs. The experiments reveal that the tool can prune out up to 27% of test objectives in a program and scale to applications of 200K lines of code.

Published
2017
Full Text
View/download PDF

9. Verification Coverage for Combining Test and Proof

Author

Le, Viet Hoang, Correnson, Loïc, Signoles, Julien, Wiels, Virginie, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Dubois, Catherine, editor, and Wolff, Burkhart, editor

Published
2018
Full Text
View/download PDF

10. Qed. Computing What Remains to Be Proved

Author

Correnson, Loïc, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Kobsa, Alfred, editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Weikum, Gerhard, editor, Badger, Julia M., editor, and Rozier, Kristin Yvonne, editor

Published
2014
Full Text
View/download PDF

12. Verification of Numerical Programs: From Real Numbers to Floating Point Numbers

Author

Goodloe, Alwyn E., Muñoz, César, Kirchner, Florent, Correnson, Loïc, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Brat, Guillaume, editor, Rungta, Neha, editor, and Venet, Arnaud, editor

Published
2013
Full Text
View/download PDF

13. Combining Analyses for C Program Verification

Author

Correnson, Loïc, Signoles, Julien, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Stoelinga, Mariëlle, editor, and Pinger, Ralf, editor

Published
2012
Full Text
View/download PDF

14. Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software

Author

Bonichon, Richard, Canet, Géraud, Correnson, Loïc, Goubault, Eric, Haucourt, Emmanuel, Hirschowitz, Michel, Labbé, Sébastien, Mimram, Samuel, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Flammini, Francesco, editor, Bologna, Sandro, editor, and Vittorini, Valeria, editor

Published
2011
Full Text
View/download PDF

15. The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform.

Author

BAUDIN, PATRICK, BOBOT, FRANÇOIS, BÜHLER, DAVID, CORRENSON, LOÏC, KIRCHNER, FLORENT, KOSMATOV, NIKOLAI, MARONEZE, ANDRÉ, PERRELLE, VALENTIN, PREVOSTO, VIRGILE, SIGNOLES, JULIEN, and WILLIAMS, NICKY

Subjects
C (Computer program language), PROGRAMMING languages, PLUG-ins (Computer programs), SOFTWARE verification, COMPUTER programming
Abstract

The article criticizes aspects of the computer programming language C with a focus on the use of the Frama-C26 code analysis platform to proactively address illegal programs written in C. A gallery of Frama-C26 plug-ins for varying analyses and use cases including undefined behavior, verification of functional properties, and test case generation is provided. The use of Frama-C26 in education as well as industrial collaboration is outlined.

Published
2021
Full Text
View/download PDF

16. Equational Semantics

Author

Correnson, Loîc, Duris, Etienne, Parigot, Didier, Roussel, Gilles, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Cortesi, Agostino, editor, and Filé, Gilberto, editor

Published
1999
Full Text
View/download PDF

20. Verication Coverage for Combining Test and Proof

Author

Hoang Le, Viet, Correnson, Loïc, Signoles, Julien, and Wiels, Virginie

Subjects
Combining test and proof, Coverage criteria
Abstract

The V&V practices of safety-critical industries (e.g. avionics) are currently based on either unit testing or unit proof to verify that a function satisfies its low-level requirements in order to be compliant with the highest certification levels[26] (e.g. DO-178C level A for avionic software). In this context, the verification engineer must assess sufficient coverage of both code (structural coverage) and specification (functional coverage). However, there is no shared method for test and proof to measure structural coverage. In practice, this prevents the verification engineer from combining test and automatic proof to verify low-level requirements of a common piece of code in order to mitigate the verification cost. This paper fills this gap between test and proof by introducing a new notion of verification coverage based on mutation coverage. It subsumes functional coverage and structural coverage for both unit testing and unit proof. Consequently, it allows the verification engineer to mix test tools and automatic provers in the verification process for the sake of reducing verification cost, in the sense that the more automation is used during the verification, the less resource is spent to verify the program.

Published
2018
Full Text
View/download PDF

21. Proving Properties of Reactive Programs From C to Lustre

Author

Blanc, B., Correnson, Loïc, Dargaye, Zaynah, Gassino, J., Marre, B., 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), Institut de Radioprotection et de Sûreté Nucléaire (IRSN), and Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
Reactive Programs, Scade, Lustre, Functional and Temporal Properties, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Formal Methods, Embedded C
Abstract

International audience; In critical embedded software, proving functional properties of programs is a major area where formal methods are applied with an increasing success. Anyway, the more a property is complex, the more a high-level formal model of the software and its environment is required. However, in an industrial setting, such a model is not always available, or cannot be used for independent verification. We propose here a new route, where a high-level Lustre model is extracted from a C source program. Thus, high-level functional properties can be specified in Lustre and proved on this extracted model, hence on the real code, without requiring any additional formal documentation.

Published
2018

23. 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

24. 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

25. Spreading Static Analysis with Frama-C in Industrial Contexts

Author

Duprat, Stéphane, Moya Lamiel, Victoria, Kirchner, Florent, Correnson, Loïc, Delmas, David, Atos Intégration SAS, Atos, 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), AIRBUS Operations SAS, Toulouse, and Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
embedded system, ACSL, safety critical software, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, abstract interpretation, Static analysis, runtime error, modular analysis, Frama-C, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

International audience; This article deals with the usage of Frama-C to detect runtime-errors. As static analysis for runtime-error detection is not a novelty, we will present significant new usages in industrial contexts, which represent a change in the ways this kind of tool is employed. The main goal is to have a scalable methodology for using static analysis through the development process and by a development team. This goal is achieved by performing analysis on partial pieces of code, by using the ACSL language for interface definitions, by choosing a bottom-up strategy to process the code, and by enabling a well-balanced definition of actors and skills. The methodology, designed during the research project U3CAT, has been applied in industrial contexts with good results as for the quality of verifications and for the performance in the industrial process.

Published
2016

26. Symbolic Composition

Author

Correnson, Loïc, Duris, Étienne, Parigot, Didier, Roussel, Gilles, Syntactic Tools for Program Construction and Analysis (OSCAR), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire d'Informatique Gaspard-Monge (LIGM), Centre National de la Recherche Scientifique (CNRS)-Fédération de Recherche Bézout-ESIEE Paris-École des Ponts ParisTech (ENPC)-Université Paris-Est Marne-la-Vallée (UPEM), INRIA, and Université Paris-Est Marne-la-Vallée (UPEM)-École des Ponts ParisTech (ENPC)-ESIEE Paris-Fédération de Recherche Bézout-Centre National de la Recherche Scientifique (CNRS)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, ATTRIBUTE GRAMMARS, PARTIAL EVALUATION, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], DEFORESTATION, FUNCTIONAL PROGRAMMING, PROGRAM TRANSFORMATION
Abstract

Projet OSCAR; The deforestation of a functional program is a transformation which gets rid ofintermediate data structures constructions that appear when two functions are composed. The descriptional composition, initially introduced by Ganzinger and Giegerich, is a deforestation method dedicated to the composition of two attribute grammars. This article presents a new functional deforestation technique, called symbolic composition, based on the descriptional composition mechanism, but extending it. An automatic translation from a functional program into an equivalent attribute grammar allows symbolic composition to be applied, and then the result can be translated back into a functional program. This yields a sourceto source functional program transformation. The resulting deforestation method provides a better deforestation than other existing functional techniques. Symbolic composition, that uses the declarative and descriptional features of attribute grammars is intrinsically more powerful than categorical-flavored transformations, whose recursion schemes are set by functors. These results tend to show that attribute grammars are a simple intermediate representation, particularly well-suited for program transformations.

Published
1998

27. 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

29. 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

30. Declarative Program Transformation: A Deforestation Case-Study.

Author

Nadathur, Gopalan, Correnson, Loïc, Duris, Etienne, Parigot, Didier, and Roussel, Gilles

Abstract

Software engineering has to reconcile modularity with efficiency. One way to grapple with this dilemma is to automatically transform a modular-specified program into an efficient-implementable one. This is the aim of deforestation transformations which get rid of intermediate data structure constructions that occur when two functions are composed. Beyond classical compile time optimization, these transformations are undeniable tools for generic programming and software component specialization. Despite various and numerous research works in this area, general transformation methods cannot deforest some non-trivial intermediate constructions. Actually, these recalcitrant structures are built inside accumulating parameters and then, they follow a construction scheme which is independent from the function scheme itself. Known deforestation methods are too much tied to fixed recursion schemes to be able to deforest these structures. In this article, we show that a fully declarative approach of program transformation allows new deforestation sites to be detected and treated. We present the principle of the symbolic composition, based on the attribute grammar formalism, with an illustrative running example stemming from a typical problem of standard functional deforestations. [ABSTRACT FROM AUTHOR]

Published
1999
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results