Sites Inria

English version

Equipe de recherche PROVAL

Publications de l'équipe PROVAL

2018

Pré-publication, Document de travail

titre
A Toolchain to Produce Correct-by-Construction OCaml Programs
auteur
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, Mário Pereira, Simão Melo de Sousa
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01783851/file/main.pdf BibTex

2012

Article dans une revue

titre
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation
auteur
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (3:16), pp.1-29. ⟨http://www.lmcs-online.org/ojs/viewarticle.php?id=1037&layout=abstract&iid=40⟩. ⟨10.2168/LMCS-8(3:16)2012⟩
Accès au bibtex
https://arxiv.org/pdf/1207.3262 BibTex

Communication dans un congrès

titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00726631/file/final.pdf BibTex
titre
Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
auteur
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, Fatiha Zaïdi
article
CAV, Jul 2012, Berkeley, California, United States. pp.718-724
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00799272/file/tool.pdf BibTex
titre
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
auteur
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
article
Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, 〈10.1007/978-3-642-31365-3_8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00687640/file/main.pdf BibTex
titre
Discharging Proof Obligations from Atelier B using Multiple Automated Provers
auteur
David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka
article
Steve Reeves and Elvinia Riccobene. ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy. Springer, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00681781/file/main.pdf BibTex
titre
A Semantic Proof that Reducibility Candidates entail Cut Elimination
auteur
Denis Cousineau, Olivier Hermant
article
23rd International Conference on Rewriting Techniques and Applications (RTA'12), May 2012, Nagoya, Japan. pp.133--148, ⟨10.4230/LIPIcs.RTA.2012.133⟩
Accès au texte intégral et bibtex
https://hal-mines-paristech.archives-ouvertes.fr/hal-00743284/file/SemanticProof.pdf BibTex
titre
Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert
auteur
Catherine Lelay, Guillaume Melquiond
article
JFLA - Journées Francophone des Langages Applicatifs - 2012, Feb 2012, Carnac, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642206/file/lelay.pdf BibTex
titre
Efficient Padding Oracle Attacks on Cryptographic Hardware
auteur
Romain Bardou, Riccardo Focardi, Yusuke Kawamoto, Lorenzo Simionato, Graham Steel, Joe-Kai Tsay
article
CRYPTO, 2012, Unknown, Afghanistan. pp.608--625
Accès au bibtex
BibTex

Rapport

titre
Weakest Precondition Calculus, Revisited using Why3
auteur
Claude Marché, Asma Tafat
article
[Research Report] RR-8185, INRIA. 2012, pp.32
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00766171/file/RR-8185.pdf BibTex
titre
Reasoning with Triggers
auteur
Claire Dross, Sylvain Conchon, Andrei Paskevich
article
[Research Report] RR-7986, INRIA. 2012, pp.29
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00703207/file/RR-7986.pdf BibTex

Thèse

titre
Taking architecture and compiler into account in formal proofs of numerical programs
auteur
Thi Minh Tuyen Nguyen
article
Other [cs.OH]. Université Paris Sud - Paris XI, 2012. English. ⟨NNT : 2012PA112090⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00710193/file/VD2_NGUYEN_Thi-Minh-Tuyen_11062012.pdf BibTex

Pré-publication, Document de travail

titre
Towards Provably Robust Watermarking
auteur
David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring
article
2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00682398/file/techreport.pdf BibTex

2011

Article dans une revue

titre
Exact and Approximated error of the FMA
auteur
Sylvie Boldo, Jean-Michel Muller
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2011, 60 (2), pp.157-164. ⟨10.1109/TC.2010.139⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00429617/file/fma_err.pdf BibTex
titre
Certifying the floating-point implementation of an elementary function using Gappa
auteur
Florent de Dinechin, Christoph Lauter, Guillaume Melquiond
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2011, 60 (2), pp.242-253. ⟨10.1109/TC.2010.128⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/ensl-00200830/file/10-tc.pdf BibTex
titre
Formal verification of numerical programs: from C annotated programs to mechanical proofs
auteur
Sylvie Boldo, Claude Marché
article
Mathematics in Computer Science, Springer, 2011, 5, pp.377-393
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00777605/file/boldo11mcs.pdf BibTex
titre
Proofs of numerical programs when the compiler optimizes
auteur
Sylvie Boldo, Thi Minh Tuyen Nguyen
article
Innovations in Systems and Software Engineering, Springer Verlag, 2011, 7, pp.151-160
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00777639/file/ISSE.pdf BibTex

Communication dans un congrès

titre
Hardware-Dependent Proofs of Numerical Programs
auteur
Thi Minh Tuyen Nguyen, Claude Marché
article
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772508/file/main.pdf BibTex
titre
Flocq: A Unified Library for Proving Floating-point Algorithms in Coq
auteur
Sylvie Boldo, Guillaume Melquiond
article
Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Jul 2011, Tübingen, Germany. pp.243-252, ⟨10.1109/ARITH.2011.40⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534854/file/11-arith20-article.pdf BibTex
titre
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
auteur
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
article
TACAS - Tools and Algorithms for the Construction and Analysis of Systems, 2011, Saarbrücken, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00777663/file/conchon11tacas.pdf BibTex
titre
Automated Certified Proofs with CiME3
auteur
Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain
article
RTA - 22nd International Conference on Rewriting Techniques and Applications, 2011, Novi Sad, Serbia
Accès au bibtex
BibTex
titre
Correct Code Containing Containers
auteur
Claire Dross, Jean-Christophe Filliâtre, Yannick Moy
article
TAP - 5th International Conference on Tests and Proofs, 2011, Zurich, Switzerland
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00777683/file/dross11tap.pdf BibTex
titre
Why3: Shepherd Your Herd of Provers
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
article
Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00790310/file/main.pdf BibTex

Direction d'ouvrage, Proceedings, Dossier

titre
Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010
auteur
Bernhard Beckert, Claude Marché
article
Bernhard Beckert and Claude Marché. 6528, Springer, pp.200, 2011
Accès au bibtex
BibTex

Rapport

titre
A Certified Multi-prover Verification Condition Generator
auteur
Paolo Herms, Claude Marché, Benjamin Monate
article
[Research Report] RR-7793, INRIA. 2011, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00639977/file/RR-7793.pdf BibTex
titre
Binary Heaps Formally Verified in Why3
auteur
Asma Tafat, Claude Marché
article
[Research Report] RR-7780, INRIA. 2011, pp.33
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00636083/file/main.pdf BibTex
titre
Automated Generation of Loop Invariants using Predicate Abstraction
auteur
Krishnamani Kalyanasundaram, Claude Marché
article
[Research Report] RR-7714, INRIA. 2011, pp.32
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00615623/file/main.pdf BibTex
titre
Proving Floating-Point Numerical Programs by Analysis of their Assembly Code
auteur
Nguyen Thi Minh Tuyen, Claude Marché
article
[Research Report] RR-7655, INRIA. 2011, pp.61
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00602266/file/main.pdf BibTex
titre
Expressing Polymorphic Types in a Many-Sorted Language
auteur
François Bobot, Andrei Paskevich
article
[Research Report] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00591414/file/polyfol.pdf BibTex

Thèse

titre
Verification of Pointer Programs Using Regions and Permissions
auteur
Romain Bardou
article
Other [cs.OH]. Université Paris Sud - Paris XI, 2011. English. ⟨NNT : 2011PA112220⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00647331/file/VD2_BARDOU_ROMAIN_14102011.pdf BibTex
titre
Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
auteur
Stephane Lescuyer
article
Other [cs.OH]. Université Paris Sud - Paris XI, 2011. English. ⟨NNT : 2011PA112363⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00713668/file/VA2_LESCUYER_STEPHANE_04012011.pdf BibTex

2010

Article dans une revue

titre
L'informatique
auteur
Sylvie Boldo
article
Qui veut gagner des neurones?, Universcience, 2010, 5-12, ⟨http://www.universcience.tv/media/1340/l-informatique.html⟩
Accès au bibtex
BibTex
titre
C'est la faute à l'ordinateur !
auteur
Sylvie Boldo
article
Interstices, INRIA, 2010
Accès au bibtex
BibTex
titre
Certification of bounds on expressions involving rounded operators
auteur
Marc Daumas, Guillaume Melquiond
article
ACM Transactions on Mathematical Software, Association for Computing Machinery, 2010, 37 (1), pp.1-20. ⟨10.1145/1644001.1644002⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00127769/file/article.pdf BibTex
titre
Modular inference of subprogram contracts for safety checking
auteur
Yannick Moy, Claude Marché
article
Journal of Symbolic Computation, Elsevier, 2010, 45, pp.1184-1211
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534331/file/YJSCO1169.pdf BibTex

Communication dans un congrès

titre
Ground Associative and Commutative Completion Modulo Shostak Theories
auteur
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
article
LPAR, Oct 2010, Yogyakarta, Indonesia
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00535652/file/conchon-lpar17-short.pdf BibTex
titre
Formal verification of numerical programs: from C annotated programs to Coq proofs
auteur
Sylvie Boldo
article
NSV-3: Third International Workshop on Numerical Software Verification, Jul 2010, Edinburgh, Scotland, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534400/file/article.pdf BibTex
titre
Formal proof of a wave equation resolution scheme: the method error
auteur
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
article
ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00450789/file/RR-7181.pdf BibTex
titre
Multi-prover verification of floating-point programs
auteur
Ali Ayad, Claude Marché
article
Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534333/file/main.pdf BibTex
titre
Certification of a chain for deductive program verification
auteur
Paolo Herms
article
2nd Coq Workshop, satellite of ITP'10, Jul 2010, Edinburgh, United Kingdom
Accès au bibtex
BibTex
titre
A refinement methodology for object-oriented programs
auteur
Asma Tafat, Sylvain Boulmé, Claude Marché
article
Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. pp.143--159
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534336/file/13.pdf BibTex
titre
Lucy-n: a n-Synchronous Extension of Lustre
auteur
Louis Mandel, Florence Plateau, Marc Pouzet
article
Tenth International Conference on Mathematics of Program Construction (MPC 2010), Jun 2010, Québec, Canada, France. pp.288-309, 2010
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545801/file/MandelPlateauPouzet-MPC-10.pdf BibTex
titre
Hardware-independent proofs of numerical programs
auteur
Sylvie Boldo, Thi Minh Tuyen Nguyen
article
Second NASA Formal Methods Symposium (NFM 2010), NASA, Apr 2010, Washington D.C., United States. pp.14-23
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534410/file/index.pdf BibTex
titre
Specifying Generic Java Programs: two case studies
auteur
Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko
article
11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010, Mar 2010, Paphos, Cyprus. pp.92--106
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00525784/file/gmtkLDTA2010.pdf BibTex
titre
Tighter Integration of {BDDs} and {SMT} for Predicate Abstraction
auteur
Alessandro Cimatti, Anders Franzen, Alberto Griggio, Krishnamani Kalyanasundaram, Marco Roveri
article
Design, Automation & Test in Europe, Mar 2010, Dresden, Germany. pp.1707--1712
Accès au bibtex
BibTex
titre
Lucy-n~: une extension n-synchrone de Lustre
auteur
Louis Mandel, Florence Plateau, Marc Pouzet
article
Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Jan 2010, Vieux-Port La Ciotat, France, France. pp.275-306, 2010
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00545802/file/MandelPlateau-JFLA-2010.pdf BibTex
titre
Observation temps-réel de programmes Caml
auteur
Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, Guillaume Von Tokarski
article
JFLA (Journées Francophones des Langages Impératifs), INRIA, Jan 2010, Vieux-Port La Ciotat, France. pp.195-216
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00535644/file/ocamlviz-jfla2010.pdf BibTex
titre
Conteneurs de première classe en Coq
auteur
Stéphane Lescuyer
article
Journées Françaises des Langages Applicatifs, INRIA, Jan 2010, La Ciotat, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00535659/file/lescuyer.pdf BibTex
titre
A3PAT, an Approach for Certified Automated Termination Proofs
auteur
Evelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, Xavier Urbain
article
2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, ACM, Jan 2010, Madrid, Spain. pp.63-72, ⟨10.1145/1706356.1706370⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00535655/file/pepm10-contejean.pdf BibTex

Direction d'ouvrage, Proceedings, Dossier

titre
Formal Verification of Object-Oriented Software, Papers Presented at the International Conference
auteur
Bernhard Beckert, Claude Marché
article
Bernhard Beckert and Claude Marché. 2010-13, Karlsruhe University, pp.368, 2010, Karlsruhe Reports in Informatics
Accès au bibtex
BibTex

Ouvrage (y compris édition critique et traduction)

titre
Handbook of Floating-Point Arithmetic
auteur
Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, Serge Torres
article
Birkhauser Boston, pp.572, 2010
Accès au bibtex
BibTex

Poster

titre
Formal proofs of numerical programs
auteur
Nguyen Thi Minh Tuyen, Sylvie Boldo, Claude Marché
article
Forum Digitéo, Oct 2010, Palaiseau, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00536135/file/posterDIGITEO.pdf BibTex

Rapport

titre
Regions and Permissions for Verifying Data Invariants
auteur
Romain Bardou, Claude Marché
article
[Research Report] RR-7412, INRIA. 2010, pp.40
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00525384/file/RR-7412.pdf BibTex
titre
A Refinement Approach for Correct-by-Construction Object-Oriented Programs
auteur
Asma Tafat, Sylvain Boulmé, Claude Marché
article
[Research Report] RR-7310, INRIA. 2010, pp.31
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00491835/file/RR-7310.pdf BibTex

2009

Article dans une revue

titre
Floats & Ropes: a case study for formal numerical program verification
auteur
Sylvie Boldo
article
Lecture Notes in Computer Science, Springer, 2009, 36th International Colloquium on Automata, Languages and Programming, 5556, pp.91--102. ⟨10.1007/978-3-642-02930-1_8⟩
Accès au bibtex
BibTex
titre
Proofs of randomized algorithms in Coq
auteur
Philippe Audebaud, Christine Paulin-Mohring
article
Science of Computer Programming, Elsevier, 2009, ⟨10.1016/j.scico.2007.09.002⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00431771/file/postprint.pdf BibTex
titre
Kahan's algorithm for a correct discriminant computation at last formally proven
auteur
Sylvie Boldo
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2009, 58 (2), pp.220-225. ⟨10.1109/TC.2008.200⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00171497/file/boldo.pdf BibTex
titre
Formally Verified Argument Reduction with a Fused Multiply-Add
auteur
Sylvie Boldo, Marc Daumas, Ren-Cang Li
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2009, 58 (8), pp.1139-1145. ⟨10.1109/TC.2008.216⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00168401/file/BDL.pdf BibTex
titre
Computing predecessor and successor in rounding to nearest
auteur
Siegfried Rump, Paul Zimmermann, Sylvie Boldo, Guillaume Melquiond
article
BIT Numerical Mathematics, Springer Verlag, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00337537/file/RuZiBoMe08.pdf BibTex

Communication dans un congrès

titre
Who: A Verifier for Effectful Higher-order Programs
auteur
Johannes Kanig, Jean-Christophe Filliâtre
article
ACM SIGPLAN Workshop on ML, Aug 2009, Edinburgh, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00777585/file/wml09.pdf BibTex
titre
Combining Coq and Gappa for Certifying Floating-Point Programs
auteur
Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
article
16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. pp.59-74, ⟨10.1007/978-3-642-02614-0_10⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432726/file/09-calculemus-article.pdf BibTex
titre
Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic
auteur
Clément Hurlin, François Bobot, Alexander Summers
article
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09), Jul 2009, Genova, Italy
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00777577/file/size.pdf BibTex
titre
Relaxing Synchronous Composition with Clock Abstraction
auteur
Albert Cohen, Louis Mandel, Florence Plateau, Marc Pouzet
article
Hardware Design and Functional Languages Workshop, Mar 2009, York, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00645333/file/HFL09-abstract-and-slides.pdf BibTex

Chapitre d'ouvrage

titre
A constructive denotational semantics for Kahn networks in Coq
auteur
Christine Paulin-Mohring
article
Yves Bertot and Gérard Huet and Jean-Jacques Lévy and Gordon Plotkin. From Semantics to Computer Science, Cambridge University Press, pp.383-413, 2009, 9780521518253
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00431806/file/postprint.pdf BibTex

Rapport

titre
On formal methods for certifying floating-point C programs
auteur
Ali Ayad
article
[Research Report] RR-6927, INRIA. 2009, pp.34
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00383793/file/RR-6927.pdf BibTex
titre
Algebraic types and pattern matching in the logical language of the Why verification platform
auteur
Andrei Paskevich
article
[Research Report] RR-7128, INRIA. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00439232/file/RR-7128.pdf BibTex
titre
Modular Specification of Java Programs
auteur
Elena Tushkanova, Alain Giorgetti, Claude Marché, Olga Kouchnarenko
article
[Research Report] RR-7097, INRIA. 2009, pp.26
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00434452/file/RR-7097.pdf BibTex

2008

Article dans une revue

titre
Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd
auteur
Sylvie Boldo, Guillaume Melquiond
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩
Accès au texte intégral et bibtex
https://hal-ens-lyon.archives-ouvertes.fr/inria-00080427/file/odd-rounding.pdf BibTex
titre
Proving Operational Termination of Membership Equational Programs
auteur
Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain
article
Higher-Order and Symbolic Computation, Springer Verlag, 2008, 21 (1-2), pp.59-88
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00431474/file/duran08hosc.pdf BibTex

Communication dans un congrès

titre
Abstraction of Clocks in Synchronous Data-flow Systems
auteur
Albert Cohen, Louis Mandel, Florence Plateau, Marc Pouzet
article
6th Asian Symposium on Programming Languages and Systems (APLAS), Dec 2008, Bangalore, India
Accès au bibtex
BibTex
titre
A Hoare Logic for Call-by-Value Functional Programs
auteur
Yann Régis-Gianas, François Pottier
article
MPC 08 - Proceedings of the Ninth International Conference on Mathematics of Program Construction, Jul 2008, Marseille, France. pp.305--335, ⟨10.1007/978-3-540-70594-9_17⟩
Accès au bibtex
BibTex
titre
Formal proof for delayed finite field arithmetic using floating point operators
auteur
Sylvie Boldo, Marc Daumas, Pascal Giorgi
article
8th Conference on Real Numbers and Computers, Jul 2008, Saint Jacques de Compostelle, Spain. pp.113-122
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00135090/file/rnc.pdf BibTex
titre
SAT-MICRO: petit mais costaud !
auteur
Sylvain Conchon, Johannes Kanig, Stéphane Lescuyer
article
JFLA (Journées Francophones des Langages Applicatifs), INRIA, Jan 2008, Etretat, France. pp.91-106
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00202831/file/conchon.pdf BibTex
titre
Gagner en passant à la corde
auteur
Jean-Christophe Filliâtre
article
JFLA (Journées Francophones des Langages Applicatifs), INRIA, Jan 2008, Etretat, France. pp.139-152
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00202841/file/filliatre.pdf BibTex

Rapport

titre
Graph-based Reduction of Program Verification Conditions
auteur
Jean-François Couchot, Alain Giorgetti, Nicolas Stouls
article
[Research Report] RR-6702, INRIA. 2008, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00339847/file/RR-6702.pdf BibTex
titre
Directed Rounding Arithmetic Operations in C++
auteur
Guillaume Melquiond, Sylvain Pion
article
[Research Report] RR-6757, INRIA. 2008, pp.11
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00345094/file/RR-6757.pdf BibTex

2007

Communication dans un congrès

titre
The Why/Krakatoa/Caduceus platform for deductive program verification
auteur
Jean-Christophe Filliâtre, Claude Marché
article
19th International Conference on Computer Aided Verification, Jul 2007, Berlin, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00270820/file/cav.pdf BibTex
titre
Guiding the Correction of Parameterized Specifications
auteur
Jean-François Couchot, Frédéric Dadeau
article
6th international conference on integrated Formal Methods (iFM'07), Jul 2007, Oxford, United Kingdom
Accès au bibtex
BibTex

Chapitre d'ouvrage

titre
Towards Modular Algebraic Specifications for Pointer Programs: a Case Study
auteur
Claude Marché
article
Hubert Comon-Lundh and Claude Kirchner and Hélène Kirchner. Rewriting, Computation and Proof, 4600, Springer, pp.235-258, 2007, lecture notes in computer science
Accès au bibtex
BibTex

Rapport

titre
Checking C Pointer Programs for Memory Safety
auteur
Yannick Moy
article
[Research Report] RR-6334, INRIA. 2007, pp.54
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00181950/file/RR-6334.pdf BibTex

2006

Communication dans un congrès

titre
Verification of Java Card applets behavior with respect to transactions and card tears
auteur
Claude Marché, Nicolas Rousset
article
Software Engineering and Formal Methods, Sep 2006, Pune, India
Accès au bibtex
BibTex
titre
Provably Faithful Evaluation of Polynomials
auteur
Sylvie Boldo, César Muñoz
article
21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000892/file/main.pdf BibTex
titre
N-Synchronous Kahn Networks
auteur
Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, Marc Pouzet
article
POPL 2006 - 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , Jan 2006, Charleston, South Carolina, United States. pp.180--193
Accès au bibtex
BibTex

Autre publication

titre
Cantor : On Ordinal Notations
auteur
Pierre Castéran, Evelyne Contejean
article
2006
Accès au bibtex
BibTex

Rapport

titre
Mechanically proving termination using polynomial interpretations
auteur
Evelyne Contejean, Claude Marché, Ana-Paula Tomas, Xavier Urbain
article
[Intern report] 1382, 2006
Accès au bibtex
BibTex

2005

Communication dans un congrès

titre
Synchronization of Periodic Clocks
auteur
Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, Marc Pouzet
article
ACM Conference on Embedded Software (EMSOFT), 2005, Jersey City, NJ, United States. 339--342 (short paper)
Accès au bibtex
BibTex

2004

Article dans une revue

titre
The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML
auteur
Claude Marché, Christine Paulin-Mohring, Xavier Urbain
article
The Journal of Logic and Algebraic Programming, 2004, 58 (1-2), pp.89-106. ⟨10.1016/j.jlap.2003.07.006⟩
Accès au bibtex
BibTex

Suivez Inria