Skip to Main content Skip to Navigation

hal-01162661v2  Conference papers
Martin ClochardJean-Christophe FilliâtreAndrei Paskevich. 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
Jean-Christophe FilliâtreMário Pereira. A Modular Way to Reason About Iteration
8th NASA Formal Methods Symposium, Jun 2016, Minneapolis, United States
hal-02019195v1  Documents associated with scientific events
Christine GaßnerArno PaulyFlorian Steinberg. 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
Akitoshi KawamuraFlorian SteinbergHolger Thies. 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
Bruce KapronFlorian Steinberg. 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
Martin Clochard. 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
Eike NeumannFlorian Steinberg. 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
Martin ClochardJean-Christophe FilliâtreClaude MarchéAndrei Paskevich. 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
Florian SteinbergHolger Thies. 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
Florian Faissole. 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
Sylvain ConchonDavid DeclerckFatiha Zaïdi. 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
Thibault HilaireHacène OuziaBenoit Lopez. 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-01350225v1  Journal articles
Sylvie Boldo. Un algorithme de découpe de gâteau
Interstices, INRIA, 2010
hal-02421484v1  Reports
Léo Andrès. 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
Cláudio Belo LourençoMaria FradeJorge Sousa Pinto. 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
Jean-Christophe Filliâtre. 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
Jean-Christophe Filliâtre. Deductive Verification of OCaml Libraries
iFM 2019 - International Conference on integrated Formal Methods, Dec 2019, Bergen, Norway
hal-02420588v1  Conference papers
Sylvain ConchonMattias Roux. Reasoning about Universal Cubes in MCMT
ICFEM 2019 - 21st International Conference on Formal Engineering Methods, Nov 2019, Shenzhen, China. pp.270--285
hal-01350274v1  Journal articles
Sylvie Boldo. Demandez le programme
Interstices, INRIA, 2009
tel-00874679v1  Theses
Asma Tafat. Preuves par raffinement de programmes avec pointeurs
Autre [cs.OH]. Université Paris Sud - Paris XI, 2013. Français. ⟨NNT : 2013PA112141⟩
hal-02276257v1  Conference papers
Benedikt BeckerClaude Marché. 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
Sylvain ConchonGiorgio DelzannoAngelo Ferrando. Parameterized Verification of Topology-sensitive Distributed Protocols goes Declarative
International Conference on Networked Systems (NETYS), May 2018, Essaouira, Morocco
hal-01653153v1  Conference papers
Raphaël Rieu-Helft. 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
Florian FaissoleBas Spitters. 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
Sylvain ConchonAmit GoelSava KrstićAlain MebsoutFatiha Zaïdi. 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
Sylvain ConchonAlain MebsoutFatiha Zaïdi. 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
Claude MarchéAsma Tafat. 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
Martin ClochardLéon GondelmanMário Pereira. The Matrix Reproved (Verification Pearl)
VSTTE 2016, Jul 2016, Toronto, Canada
hal-01404935v1  Conference papers
Martin Clochard. Preuves taillées en biseau
vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Jan 2017, Gourette, France