Filtrer vos résultats
- 50
- 11
- 39
- 6
- 5
- 5
- 2
- 2
- 1
- 1
- 4
- 1
- 61
- 3
- 1
- 4
- 2
- 3
- 6
- 4
- 3
- 1
- 5
- 2
- 4
- 8
- 4
- 3
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 43
- 18
- 58
- 47
- 12
- 6
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 61
- 15
- 11
- 7
- 7
- 5
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
61 résultats
Why3 version 1.0France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
Brevet
hal-03136256v1
|
|||
|
|
A Toolchain to Produce Verified OCaml Libraries2020
Pré-publication, Document de travail
hal-01783851v2
|
||
Numérique et Sciences Informatiques, 24 leçons avec exercices corrigés. TerminaleEllipses, pp.526, 2020, 9782340038554
Ouvrages
hal-03023099v1
|
|||
|
|
Why3: Shepherd Your Herd of ProversBoogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64
Communication dans un congrès
hal-00790310v1
|
||
|
|
The Spirit of Ghost CodeFormal Methods in System Design, 2016, 48 (3), pp.152-174. ⟨10.1007/s10703-016-0243-x⟩
Article dans une revue
hal-01396864v1
|
||
Real-Time Monitoring of Ocaml programsJFLA 2010, Jan 2010, Vieux-Port La Ciotat, France. pp.159-185
Communication dans un congrès
hal-00941407v1
|
|||
|
|
A Modular Way to Reason About Iteration8th NASA Formal Methods Symposium, Jun 2016, Minneapolis, United States
Communication dans un congrès
hal-01281759v2
|
||
|
|
Ortac: Runtime Assertion Checking for OCamlRV'21 - 21st International Conference on Runtime Verification, Oct 2021, Los Angeles, CA, United States
Communication dans un congrès
hal-03252901v2
|
||
|
|
Gagner en passant à la cordeJFLA (Journées Francophones des Langages Applicatifs), INRIA, Jan 2008, Etretat, France. pp.139-152
Communication dans un congrès
inria-00202841v1
|
||
|
|
The Why/Krakatoa/Caduceus platform for deductive program verification19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany
Communication dans un congrès
inria-00270820v1
|
||
|
|
Why3 -- Where Programs Meet ProversESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy
Communication dans un congrès
hal-00789533v1
|
||
|
|
The COST IC0701 Verification Competition 2011Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy
Communication dans un congrès
hal-00789525v1
|
||
|
|
Formalizing Semantics with an Automatic Program Verifier6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria
Communication dans un congrès
hal-01067197v1
|
||
|
|
Design of a proof assistant: Coq version 7[Research Report] Université Paris-Sud. 2000
Rapport
hal-02890416v1
|
||
|
|
Separation Predicates: a Taste of Separation Logic in First-Order Logic14th International Conference on Formal Ingineering Methods (ICFEM), Nov 2012, Kyoto, Japan. pp.167-181, ⟨10.1007/978-3-642-34281-3_14⟩
Communication dans un congrès
hal-00825088v1
|
||
|
|
Producing All Ideals of a Forest, Formally (Verification Pearl)VSTTE 2016, Jul 2016, Toronto, Canada. pp.46 - 55, ⟨10.1007/978-3-319-48869-1_4⟩
Communication dans un congrès
hal-01316859v2
|
||
|
|
Wasocaml: compiling OCaml to WebAssemblyIFL 2023 - The 35th Symposium on Implementation and Application of Functional Languages, João Saraiva; João Fernandes, Aug 2023, Braga, Portugal
Communication dans un congrès
hal-04311345v2
|
||
|
|
Vérification de programmes OCaml fortement impératifs avec Why3JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. pp.1-14
Communication dans un congrès
hal-01649989v2
|
||
Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Première.Ellipses, 2019
Ouvrages
hal-02379073v1
|
|||
Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec PythonEyrolles, pp.1-390, 2013, 978-2-212-13700-2
Ouvrages
hal-00880268v1
|
|||
|
|
Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup[Rapport Technique] Université Paris-Saclay. 2020
Rapport
hal-02447409v1
|
||
|
|
Optimizing Prestate Copies in Runtime Verification of Function PostconditionsRV 2022 - 22nd International Conference on Runtime Verification, Sep 2022, Tbilisi, Georgia
Communication dans un congrès
hal-03690675v2
|
||
|
|
Semi-persistent Data StructuresEuropean Symposium on Programming, Mar 2008, Budapest, Hungary. pp.322-336, ⟨10.1007/978-3-540-78739-6_25⟩
Communication dans un congrès
hal-04045849v1
|
||
|
|
Who: A Verifier for Effectful Higher-order ProgramsACM SIGPLAN Workshop on ML, Aug 2009, Edinburgh, United Kingdom
Communication dans un congrès
hal-00777585v1
|
||
|
|
Functors for Proofs and Programs13th European Symposium on Programming, ESOP 2004, Feb 2004, Barcelona, Spain. pp.370-384, ⟨10.1007/b96702⟩
Communication dans un congrès
hal-00150913v1
|
||
Apprendre à programmer avec OCamlEyrolles, pp.429, 2014, Noire, 9782212136784
Ouvrages
hal-01063853v1
|
|||
|
|
Mesurer la hauteur d'un arbreJLFA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France
Communication dans un congrès
hal-02315541v2
|
||
|
|
Wave equation numerical resolution: a comprehensive mechanized proof of a C programJournal of Automated Reasoning, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩
Article dans une revue
hal-00649240v3
|
||
|
|
The Why3 platform 0.812013
Autre publication scientifique
hal-00822856v1
|
||
|
|
Why3, une plateforme pour la vérification déductiveJournées FAC 2023, groupe IFSE du RTRA STAE, Apr 2023, Toulouse, France
Communication dans un congrès
hal-04060570v1
|