 |
 |
 |
|
|
||
|---|---|---|
|
hal-01162661v2
Conference papers
How to avoid proving the absence of integer overflows 7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States |
||
|
hal-01281759v2
Conference papers
A Modular Way to Reason About Iteration 8th NASA Formal Methods Symposium, Jun 2016, Minneapolis, United States |
||
|
hal-02019195v1
Documents associated with scientific events
Comparing integrability and measurability in different models of computation CIE 2018 - 14th Conference on Computability in Europe, Jul 2018, Kiel, Germany |
||
|
hal-02019142v1
Conference papers
Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving Wollic 2018 - International Workshop on Logic, Language, Information, and Computation, Jul 2018, Bogota, Colombia. pp.223-236, ⟨10.1007/978-3-662-57669-4_13⟩ |
||
|
hal-02019150v1
Conference papers
Type-two polynomial-time and restricted lookahead LICS 2018 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.579-588, ⟨10.1145/3209108.3209124⟩  |
||
|
hal-01067217v1
Conference papers
Automatically verified implementation of data structures based on AVL trees 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria |
||
|
hal-02019134v1
Conference papers
Parametrised second-order complexity theory with applications to the study of interval computation DICE 2018 - Developments in Implicit Computational Complexity, Apr 2018, Thesaloniki, Greece |
||
|
hal-01067197v1
Conference papers
Formalizing Semantics with an Automatic Program Verifier 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria |
||
|
hal-02019174v1
Documents associated with scientific events
Some formal proofs of isomorphy and discontinuity MLA 2019 - Third Workshop on Mathematical Logic and its Applications, Mar 2019, Nancy, France |
||
|
hal-01630411v1
Conference papers
Formalization and closedness of finite dimensional subspaces SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7 |
||
|
hal-01767064v1
Conference papers
Compiling Parameterized X86-TSO Concurrent Programs to Cubicle- W 19th International Conference on Formal Methods and Software Engineering, Nov 2017, Xi'an, China. pp.88-104, ⟨10.1007/978-3-319-68690-5_6⟩ |
||
|
hal-02393851v1
Conference papers
Optimal Word-Length Allocation for the Fixed-Point Implementation of Linear Filters and Controllers ARITH 2019 - IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.175-182, ⟨10.1109/ARITH.2019.00040⟩ |
||
|
hal-02421484v1
Reports
Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification [Rapport de recherche] Université Paris Sud (Paris 11) - Université Paris Saclay. 2019 |
||
|
hal-02431769v1
Conference papers
A Generalized Program Verification Workflow Based on Loop Elimination and SA Form FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, May 2019, Montreal, Canada |
||
|
hal-02406208v1
Conference papers
Retour sur 25 ans de programmation avec OCaml JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France |
||
|
hal-02406253v1
Conference papers
Deductive Verification of OCaml Libraries iFM 2019 - International Conference on integrated Formal Methods, Dec 2019, Bergen, Norway |
||
|
hal-02420588v1
Conference papers
Reasoning about Universal Cubes in MCMT ICFEM 2019 - 21st International Conference on Formal Engineering Methods, Nov 2019, Shenzhen, China. pp.270--285 |
||
|
tel-00874679v1
Theses
Preuves par raffinement de programmes avec pointeurs Autre [cs.OH]. Université Paris Sud - Paris XI, 2013. Français. ⟨NNT : 2013PA112141⟩ |
||
|
hal-02276257v1
Conference papers
Ghost Code in Action: Automated Verification of a Symbolic Interpreter VSTTE 2019 - 11th Working Conference on Verified Software: Tools, Techniques and Experiments, Jul 2019, New York, United States |
||
|
hal-02001652v1
Conference papers
Parameterized Verification of Topology-sensitive Distributed Protocols goes Declarative International Conference on Networked Systems (NETYS), May 2018, Essaouira, Morocco |
||
|
hal-01653153v1
Conference papers
Un mécanisme d'extraction vers C pour Why3 29èmes Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France |
||
|
hal-01405762v1
Conference papers
Synthetic topology in HoTT for probabilistic programming The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Jan 2017, Paris, France |
||
|
hal-00924640v1
Conference papers
Invariants for Finite Instances and Beyond Formal Methods in Computer-Aided Design (FMCAD), Oct 2013, Portland, Oregon, United States. pp.61-68, ⟨10.1109/FMCAD.2013.6679392⟩ |
||
|
hal-00778832v1
Conference papers
Vérification de systèmes paramétrés avec Cubicle JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France |
||
|
hal-00778791v1
Conference papers
Calcul de plus faible précondition, revisité en Why3 JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France |
||
|
hal-01316902v2
Conference papers
The Matrix Reproved (Verification Pearl) VSTTE 2016, Jul 2016, Toronto, Canada |
||
|
hal-01404935v1
Conference papers
Preuves taillées en biseau vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Jan 2017, Gourette, France |
||
|
|
||
