Search

Your search keyword '"Filliâtre, Jean-Christophe"' showing total 191 results
Start Over Author "Filliâtre, Jean-Christophe"

Refine your results

more »

more »

more »

more »
191 results on '"Filliâtre, Jean-Christophe"'

2. Ortac: Runtime Assertion Checking for OCaml (Tool Paper)

Author

Filliâtre, Jean-Christophe, Pascutto, Clément, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Feng, Lu, editor, and Fisman, Dana, editor

Published
2021
Full Text
View/download PDF

3. Abstraction and Genericity in Why3

Author

Filliâtre, Jean-Christophe, Paskevich, Andrei, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Margaria, Tiziana, editor

Published
2020
Full Text
View/download PDF

6. GOSPEL—Providing OCaml with a Formal Specification Language

Author

Charguéraud, Arthur, Filliâtre, Jean-Christophe, Lourenço, Cláudio, Pereira, Mário, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, ter Beek, Maurice H., editor, McIver, Annabelle, editor, and Oliveira, José N., editor

Published
2019
Full Text
View/download PDF

7. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program

Author

Boldo, Sylvie, Clément, François, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, and Weis, Pierre

Subjects
Mathematics - Numerical Analysis, Computer Science - Logic in Computer Science
Abstract

Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved., Comment: N° RR-8197 (2012). arXiv admin note: text overlap with arXiv:1112.1795

Published
2012

9. Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program

Author

Boldo, Sylvie, Clement, Francois, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, and Weis, Pierre

Subjects
Computer Science - Logic in Computer Science, Mathematics - Numerical Analysis
Abstract

We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked., Comment: No. RR-7826 (2011)

Published
2011
Full Text
View/download PDF

10. Formal Proof of a Wave Equation Resolution Scheme: the Method Error

Author

Boldo, Sylvie, Clément, François, Filliâtre, Jean-Christophe, Mayero, Micaela, Melquiond, Guillaume, and Weis, Pierre

Subjects
Computer Science - Logic in Computer Science, Mathematics - Numerical Analysis
Abstract

Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked., Comment: replaces arXiv:1001.4898

Published
2010
Full Text
View/download PDF

12. A Modular Way to Reason About Iteration

Author

Filliâtre, Jean-Christophe, Pereira, Mário, 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, Rayadurgam, Sanjai, editor, and Tkachuk, Oksana, editor

Published
2016
Full Text
View/download PDF

13. How to Avoid Proving the Absence of Integer Overflows

Author

Clochard, Martin, Filliâtre, Jean-Christophe, Paskevich, Andrei, 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, Gurfinkel, Arie, editor, and Seshia, Sanjit A., editor

Published
2016
Full Text
View/download PDF

14. Producing All Ideals of a Forest, Formally (Verification Pearl)

Author

Filliâtre, Jean-Christophe, Pereira, Mário, 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, Blazy, Sandrine, editor, and Chechik, Marsha, editor

Published
2016
Full Text
View/download PDF

15. Why3, une plateforme pour la vérification déductive

Author

Filliâtre, Jean-Christophe, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and groupe IFSE du RTRA STAE

Subjects
[INFO]Computer Science [cs]
Abstract

National audience; Dans cet exposé, nous présentons l'outil Why3, une plateforme pour la vérification déductive de programmes développée au Laboratoire Méthodes Formelles (Université Paris-Saclay, CNRS, ENS Paris-Saclay / Inria Saclay). Cette plateforme est utilisée dans les milieux académiques et industriels pour la vérification d'algorithmes, de codes écrits dans langages tels que C, Ada ou OCaml, ou encore lavérification de protocoles cryptographiques. La plateforme Why3 est également exploitée pour enseigner la vérification de programmes. Cet exposé met en avant les atouts de la plateforme Why3 et décrit le coeur de métier de son équipe de développement.

Published
2023

16. Preserving User Proofs across Specification Changes

Author

Bobot, François, Filliâtre, Jean-Christophe, Marché, Claude, Melquiond, Guillaume, Paskevich, Andrei, 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, Cohen, Ernie, editor, and Rybalchenko, Andrey, editor

Published
2014
Full Text
View/download PDF

17. Formalizing Semantics with an Automatic Program Verifier

Author

Clochard, Martin, Filliâtre, Jean-Christophe, Marché, Claude, Paskevich, Andrei, 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, Giannakopoulou, Dimitra, editor, and Kroening, Daniel, editor

Published
2014
Full Text
View/download PDF

18. The Spirit of Ghost Code

Author

Filliâtre, Jean-Christophe, Gondelman, Léon, Paskevich, Andrei, 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, Biere, Armin, editor, and Bloem, Roderick, editor

Published
2014
Full Text
View/download PDF

19. L'arithmétique de séparation

Author

Filliâtre, Jean-Christophe, Paskevich, Andrei, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Timothy Bourke, and Delphine Demange

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

National audience; Nous, praticiens de la preuve de programmes, souhaitons que le processus de la vérification soit le plus automatique possible. Les meilleurs outils pour cela sont à l'heure actuelle les démonstrateurs SMT, qui combinent notamment la logique du premier ordre et l'arithmétique linéaire. Par opposition, le raisonnement inductif n'est pas un point fort des démonstrateurs automatiques. Or, les programmes utilisant des pointeurs le font souvent pour manipuler des structures récursives : listes, arbres, etc. Dans cet article, nous décrivons une approche qui permet d'amener la preuve de programmes avec pointeurs à la portée des démonstrateurs automatiques. L'idée consiste à projeter une structure récursive sur un domaine numérique, de sorte que les propriétés de possession et de séparation deviennent exprimables en terme de simples inégalités arithmétiques. En plus de simplifier la preuve, cela permet une spécification claire et naturelle. On illustre cette approche avec l'exemple classique du renversement en place d'une liste simplement chaînée.

Published
2023

20. One Logic to Use Them All

Author

Filliâtre, Jean-Christophe, 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, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, and Bonacina, Maria Paola, editor

Published
2013
Full Text
View/download PDF

21. Why3 — Where Programs Meet Provers

Author

Filliâtre, Jean-Christophe, Paskevich, Andrei, 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, Felleisen, Matthias, editor, and Gardner, Philippa, editor

Published
2013
Full Text
View/download PDF

22. Separation Predicates: A Taste of Separation Logic in First-Order Logic

Author

Bobot, François, Filliâtre, Jean-Christophe, 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, Aoki, Toshiaki, editor, and Taguchi, Kenji, editor

Published
2012
Full Text
View/download PDF

23. Functory: A Distributed Computing Library for Objective Caml

Author

Filliâtre, Jean-Christophe, Kalyanasundaram, K., 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, Peña, Ricardo, editor, and Page, Rex, editor

Published
2012
Full Text
View/download PDF

24. The COST IC0701 Verification Competition 2011

Author

Bormer, Thorsten, Brockschmidt, Marc, Distefano, Dino, Ernst, Gidon, Filliâtre, Jean-Christophe, Grigore, Radu, Huisman, Marieke, Klebanov, Vladimir, Marché, Claude, Monahan, Rosemary, Mostowski, Wojciech, Polikarpova, Nadia, Scheben, Christoph, Schellhorn, Gerhard, Tofan, Bogdan, Tschannen, Julian, Ulbrich, Mattias, 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, Beckert, Bernhard, editor, Damiani, Ferruccio, editor, and Gurov, Dilian, editor

Published
2012
Full Text
View/download PDF

25. Discharging Proof Obligations from Atelier B Using Multiple Automated Provers

Author

Mentré, David, Marché, Claude, Filliâtre, Jean-Christophe, Asuka, Masashi, 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, Derrick, John, editor, Fitzgerald, John, editor, Gnesi, Stefania, editor, Khurshid, Sarfraz, editor, Leuschel, Michael, editor, Reeves, Steve, editor, and Riccobene, Elvinia, editor

Published
2012
Full Text
View/download PDF

26. Verifying Two Lines of C with Why3: An Exercise in Program Verification

Author

Filliâtre, Jean-Christophe, 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, Joshi, Rajeev, editor, Müller, Peter, editor, and Podelski, Andreas, editor

Published
2012
Full Text
View/download PDF

27. Correct Code Containing Containers

Author

Dross, Claire, Filliâtre, Jean-Christophe, Moy, Yannick, 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, Gogolla, Martin, editor, and Wolff, Burkhart, editor

Published
2011
Full Text
View/download PDF

28. Informatique - MP2I/MPI - CPGE 1re et 2e années - Cours et exercices corrigés

Author

Balabonski, Thibaut, Conchon, Sylvain, Filliâtre, Jean-Christophe, Nguyen, Kim, Sartre, Laurent, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
[INFO]Computer Science [cs]
Abstract

International audience

Published
2022

30. Combining Coq and Gappa for Certifying Floating-Point Programs

Author

Boldo, Sylvie, Filliâtre, Jean-Christophe, Melquiond, Guillaume, 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, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, Carette, Jacques, editor, Dixon, Lucas, editor, Coen, Claudio Sacerdoti, editor, and Watt, Stephen M., editor

Published
2009
Full Text
View/download PDF

31. Semi-persistent Data Structures

Author

Conchon, Sylvain, Filliâtre, Jean-Christophe, 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, and Drossopoulou, Sophia, editor

Published
2008
Full Text
View/download PDF

32. The Why/Krakatoa/Caduceus Platform for Deductive Program Verification : (Tool Paper)

Author

Filliâtre, Jean-Christophe, Marché, Claude, 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, Damm, Werner, editor, and Hermanns, Holger, editor

Published
2007
Full Text
View/download PDF

34. Multi-prover Verification of C Programs

Author

Filliâtre, Jean-Christophe, Marché, Claude, 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, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Davies, Jim, editor, Schulte, Wolfram, editor, and Barnett, Mike, editor

Published
2004
Full Text
View/download PDF

36. ICS: Integrated Canonizer and Solver?

Author

Filliâtre, Jean-Christophe, Owre, Sam, Rue*B, Harald, Shankar, Natarajan, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Berry, Gérard, editor, Comon, Hubert, editor, and Finkel, Alain, editor

Published
2001
Full Text
View/download PDF

39. Ortac: Runtime Assertion Checking for OCaml

Author

Filliâtre, Jean-Christophe, Pascutto, Clément, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), and Tarides [Paris]

Subjects
OCaml, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Software Engineering, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO]Computer Science [cs], Runtime Assertion Checking
Abstract

International audience; Runtime assertion checking (RAC) is a convenient set of techniques that lets developers abstract away the process of verifying the correctness of their programs by writing formal specifications and automating their verification at runtime. In this work, we present ortac, a runtime assertion checking tool for OCaml libraries and programs. OCaml is a functional programming language in which idioms rely on an expressive type system, modules, and interface abstractions. ortac consumes interfaces annotated with type invariants and function contracts and produces code wrappers with the same signature that check these specifications at runtime. It provides a flexible framework for traditional assertion checking, monitoring misbehaviors without interruptions, and automated fuzz testing for OCaml programs. This paper presents an overview of ortac features and highlights its main design choices.

Published
2021

40. Numérique et Sciences Informatiques, 24 leçons avec exercices corrigés. Terminale

Author

Balabonski, Thibaut, Conchon, Sylvain, Filliâtre, Jean-Christophe, Nguyen, Kim, Université Paris-Saclay, Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), and Filliâtre, Jean-Christophe

Subjects
[INFO]Computer Science [cs], [INFO] Computer Science [cs], ComputingMilieux_MISCELLANEOUS
Abstract

International audience

Published
2020

41. a Coq retrospective - at the heart of Coq architecture, the genesis of version 7.0

Author

Filliâtre, Jean-Christophe, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), and Filliâtre, Jean-Christophe

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-MS] Computer Science [cs]/Mathematical Software [cs.MS], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS, [INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS]
Abstract

International audience

Published
2020

42. Mesurer la hauteur d'un arbre

Author

Filliâtre, Jean-Christophe, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), and Filliâtre, Jean-Christophe

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-DS] Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO]Computer Science [cs], [INFO] Computer Science [cs], [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract

National audience; Dans cet article, nous nous intéressons au problème du calcul de la hauteur d'un arbre. Le problème a l'air plutôt simple,à priori, puisqu'il suffit de suivre la définition mathématique avec une simple fonction récursive de quelques lignes. Néanmoins, une telle fonction peut facilement faire déborder la pile d'appels. Après avoir laissé le lecteur réfléchir a une solution, nous en discutons plusieurs, notamment au regard de ce qu'offre le langage de programmation. Ce problème illustre la difficulté qu'il peut y avoir à se passer de récursivité.

Published
2020

43. Compte-rendu de fin de projet ANR-15-CE25-0008 'VOCaL'

Author

Filliâtre, Jean-Christophe, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), LMF - Laboratoire Méthodes Formelles, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Published
2021

45. Spécialité Numérique et sciences informatiques : 24 leçons avec exercices corrigés - Terminale - 2e édition

Author

Balabonski Thibaut, Conchon Sylvain, Filliâtre Jean-Christophe, Nguyen Kim, Balabonski Thibaut, Conchon Sylvain, Filliâtre Jean-Christophe, and Nguyen Kim

Abstract

Cours structuré couvrant l'intégralité du programme de la spécialité NSI en classe de terminale. Il offre vingt-quatre leçons clés en main, accompagnées d'exercices corrigés et d'encarts thématiques et historiques permettant d'approfondir les leçons. Ce livre est constitué de quatre parties : programmation algorithmique bases de données architectures matérielles, systèmes d'exploitation et réseaux. Le site qui accompagne cet ouvrage fournit du matériel librement téléchargeable, comme du code source Python, des fichiers de données pour les projets ou encore un aide-mémoire Python.

Published
2024

50. Retour sur 25 ans de programmation avec OCaml

Author

Filliâtre, Jean-Christophe, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), 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), Centre National de la Recherche Scientifique (CNRS), and Filliâtre, Jean-Christophe

Subjects
[INFO]Computer Science [cs], [INFO] Computer Science [cs], ComputingMilieux_MISCELLANEOUS
Abstract

National audience

Published
2019

Catalog

Books, media, physical & digital resources
See catalog results