publis

[1]	Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning, 2012. Accepted for publication. http://hal.inria.fr/hal-00649240/en/. [ bib ]
[2]	François Bobot and Jean-Christophe Filliâtre. Separation predicates: a taste of separation logic in first-order logic. In 14th International Conference on Formal Ingineering Methods (ICFEM), November 2012. [ bib \| Abstract ]
[3]	Mário Pereira, Jean-Christophe Filliâtre, and Sim ao Melo de Sousa. ARMY: a deductive verification platform for ARM programs using Why3. In INForum 2012, September 2012. [ bib \| Abstract ]
[4]	Jean-Christophe Filliâtre, Andrei Paskevich, and Aaron Stump. The 2nd verified software competition: Experience report. In Vladimir Klebanov and Sarah Grebing, editors, COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems. EasyChair, 2012. [ bib \| .pdf \| Abstract ]
[5]	Jean-Christophe Filliâtre. Course notes EJCP 2012, chapter Vérification déductive de programmes avec Why3. June 2012. [ bib \| http ]
[6]	Jean-Christophe Filliâtre. Vérification déductive de programmes avec Why3, Janvier 2012. Cours aux vingt-troisièmes Journées Francophones des Langages Applicatifs. [ bib \| http ]
[7]	Jean-Christophe Filliâtre. Combining Interactive and Automated Theorem Proving in Why3 (invited talk). In Keijo Heljanko and Hugo Herbelin, editors, Automation in Proof Assistants 2012, Tallinn, Estonia, April 2012. [ bib ]
[8]	David Mentré, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. Discharging proof obligations from Atelier B using multiple automated provers. In ABZ Conference, Pisa, Italy, June 2012. [ bib \| .pdf \| Abstract ]
[9]	Jean-Christophe Filliâtre. Verifying two lines of C with Why3: an exercise in program verification. In Verified Software: Theories, Tools and Experiments (VSTTE), Philadelphia, USA, January 2012. [ bib \| .pdf \| Abstract ]
[10]	Jean-Christophe Filliâtre. Deductive software verification. International Journal on Software Tools for Technology Transfer (STTT), 13(5):397--403, August 2011. [ bib \| DOI \| http \| Abstract ]
[11]	François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroclaw, Poland, August 2011. [ bib \| .pdf \| Abstract ]
[12]	Jean-Christophe Filliâtre and K. Kalyanasundaram. Functory: A Distributed Computing Library for Objective Caml. In Trends in Functional Programming, volume 7193 of Lecture Notes in Computer Science, pages 65--81, Madrid, Spain, May 2011. [ bib \| Abstract ]
[13]	Claire Dross, Jean-Christophe Filliâtre, and Yannick Moy. Correct Code Containing Containers. In 5th International Conference on Tests & Proofs (TAP'11), Zurich, June 2011. [ bib \| Abstract ]
[14]	Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, version 1.4, 2009. http://frama-c.cea.fr/acsl.html. [ bib \| .html ]
[15]	Jean-Christophe Filliâtre and Krishnamani Kalyanasundaram. Functory : Une bibliothèque de calcul distribué pour Objective Caml. In Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib \| .pdf \| Abstract ]
[16]	M. Barbosa, J.-C. Filliâtre, J. Sousa Pinto, and B. Vieira. A Deductive Verification Platform for Cryptographic Software. In 4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33, Pisa, Italy, September 2010. Electronic Communications of the EASST. [ bib \| http ]
[17]	Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In Proceedings of the first Interactive Theorem Proving Conference, LNCS, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOL and ACL2). [ bib \| http \| Abstract ]
[18]	Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, and Guillaume Von Tokarski. Observation temps-réel de programmes Caml. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib \| .pdf \| Abstract ]
[19]	Johannes Kanig and Jean-Christophe Filliâtre. Who: A Verifier for Effectful Higher-order Programs. In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August 2009. [ bib \| .pdf \| Abstract ]
[20]	Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning. LNCS/LNAI, July 2009. [ bib \| .pdf \| Abstract ]
[21]	Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, and Stéphane Lescuyer. Faire bonne figure avec Mlpost. In Vingtièmes Journées Francophones des Langages Applicatifs, Saint-Quentin sur Isère, 2009. INRIA. [ bib \| .pdf \| Abstract ]
[22]	Jean-Christophe Filliâtre. A Functional Implementation of the Garsia--Wachs Algorithm. In ACM SIGPLAN Workshop on ML, Victoria, British Columbia, Canada, September 2008. ACM. [ bib \| .pdf \| Abstract ]
[23]	Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, 2008. Short version of [26]. [ bib \| .pdf \| Abstract ]
[24]	Jean-Christophe Filliâtre. Gagner en passant à la corde. In Dix-neuvièmes Journées Francophones des Langages Applicatifs, Étretat, France, 2008. INRIA. [ bib \| .pdf \| Abstract ]
[25]	Jean-Christophe Filliâtre. Formal Verification of MIX Programs. In Journées en l'honneur de Donald E. Knuth, Bordeaux, France, October 2007. [ bib \| .pdf \| Abstract ]
[26]	Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. Research Report 1474, LRI, Université Paris Sud, September 2007. [ bib \| .pdf \| Abstract ]
[27]	Jean-Christophe Filliâtre. Queens on a Chessboard: an Exercise in Program Verification. Unpublished, January 2007. [ bib \| .ps \| Abstract ]
[28]	Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger Hermanns, editors, 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Berlin, Germany, July 2007. Springer-Verlag. [ bib \| .pdf ]
[29]	Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In 18th IEEE International Symposium on Computer Arithmetic, Montpellier, France, June 2007. [ bib \| .pdf \| Abstract ]
[30]	Sylvain Conchon and Jean-Christophe Filliâtre. A Persistent Union-Find Data Structure. In ACM SIGPLAN Workshop on ML, pages 37--45, Freiburg, Germany, October 2007. ACM. English version of [31]. [ bib \| .pdf \| Abstract ]
[31]	Sylvain Conchon and Jean-Christophe Filliâtre. Union-Find Persistant. In Dix-huitièmes Journées Francophones des Langages Applicatifs, Aix-les-bains, France, 2007. INRIA. [ bib \| .pdf \| Abstract ]
[32]	Sylvain Conchon and Jean-Christophe Filliâtre. Type-Safe Modular Hash-Consing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. Supersedes [50]. [ bib \| .pdf \| Abstract ]
[33]	Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Trends in Functional Programming, volume 8. Intellect, 2007. [ bib ]
[34]	Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In The Eighth Symposium on Trends in Functional Programming, volume TR-SHU-CS-2007-04-1, pages XII/1--13, New York, USA, April 2007. Seton Hall University. [ bib \| .ps \| Abstract ]
[35]	Nicolas Ayache and Jean-Christophe Filliâtre. Combining the Coq Proof Assistant with First-Order Decision Procedures. Unpublished, March 2006. [ bib \| .ps \| Abstract ]
[36]	Jean-Christophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. Also LRI Research Report 1428. [ bib \| .pdf \| Abstract ]
[37]	Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors. Types for Proofs and Programs International Workshop, TYPES 2004, volume 3839 of Lecture Notes in Computer Science. Springer-Verlag, 2006. [ bib ]
[38]	Jean-Christophe Filliâtre. Itérer avec persistance. In Dix-septièmes Journées Francophones des Langages Applicatifs, Pauillac, France, 2006. INRIA. [ bib \| .ps \| Abstract ]
[39]	Jean-Christophe Filliâtre. Program Verification using Coq. Introduction to the WHY tool, August 2005. Lecture Notes, TYPES Summer School 2005 (Göteborg, Sweden). [ bib \| .ps.gz ]
[40]	Jean-Christophe Filliâtre. Introduction à la programmation fonctionnelle, 2004. Notes de cours de Master M1. [ bib \| .ps.gz ]
[41]	Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Seizièmes Journées Francophones des Langages Applicatifs, pages 79--94. INRIA, March 2005. [ bib \| .ps.gz \| Abstract ]
[42]	Jean-Christophe Filliâtre and Claude Marché. Multi-Prover Verification of C Programs. In Sixth International Conference on Formal Engineering Methods (ICFEM), volume 3308 of Lecture Notes in Computer Science, pages 15--29, Seattle, November 2004. Springer-Verlag. [ bib \| .ps.gz \| Abstract ]
[43]	J.-C. Filliâtre and P. Letouzey. Functors for Proofs and Programs. In Proceedings of The European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 370--384, Barcelona, Spain, April 2004. [ bib \| .ps.gz \| Abstract ]
[44]	J.-C. Filliâtre. Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud, March 2003. [ bib \| .ps.gz ]
[45]	J.-C. Filliâtre and F. Pottier. Producing All Ideals of a Forest, Functionally. Journal of Functional Programming, 13(5):945--956, September 2003. [ bib \| .ps.gz \| Abstract ]
[46]	J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. Deciding propositional combinations of equalities and inequalities. Unpublished, October 2001. [ bib \| .ps \| Abstract ]
[47]	J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. ICS: Integrated Canonization and Solving (Tool presentation). In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV'2001, volume 2102 of Lecture Notes in Computer Science, pages 246--249. Springer-Verlag, 2001. [ bib ]
[48]	J.-C. Filliâtre. La supériorité de l'ordre supérieur. In Journées Francophones des Langages Applicatifs, pages 15--26, Anglet, France, Janvier 2002. [ bib \| .ps.gz \| Abstract ]
[49]	J.-C. Filliâtre. Design of a proof assistant: Coq version 7. Research Report 1369, LRI, Université Paris Sud, October 2000. [ bib \| .ps.gz \| Abstract ]
[50]	J.-C. Filliâtre. Hash consing in an ML framework. Research Report 1368, LRI, Université Paris Sud, September 2000. [ bib \| .ps.gz \| Abstract ]
[51]	J.-C. Filliâtre and C. Marché. ocamlweb, a literate programming tool for Objective Caml. Available at http://www.lri.fr/~filliatr/ocamlweb/. [ bib \| http ]
[52]	J.-C. Filliâtre. Verification of Non-Functional Programs using Interpretations in Type Theory. Journal of Functional Programming, 13(4):709--745, July 2003. English translation of [55]. [ bib \| .ps.gz \| Abstract ]
[53]	J.-C. Filliâtre. Formal Proof of a Program: Find. Science of Computer Programming, 64:332--240, 2006. [ bib \| DOI \| .ps \| Abstract ]
[54]	J.-C. Filliâtre. A theory of monads parameterized by effects. Research Report 1367, LRI, Université Paris Sud, November 1999. [ bib \| .ps.gz \| Abstract ]
[55]	J.-C. Filliâtre. Preuve de programmes impératifs en théorie des types. Thèse de doctorat, Université Paris-Sud, July 1999. [ bib \| .ps.gz \| Abstract ]
[56]	J.-C. Filliâtre and N. Magaud. Certification of sorting algorithms in the system Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999. [ bib \| .ps.gz \| Abstract ]
[57]	J.-C. Filliâtre. Proof of Imperative Programs in Type Theory. In International Workshop, TYPES '98, Kloster Irsee, Germany, volume 1657 of Lecture Notes in Computer Science. Springer-Verlag, March 1998. [ bib \| .ps.gz \| Abstract ]
[58]	J.-C. Filliâtre. Finite Automata Theory in Coq: A constructive proof of Kleene's theorem. Research Report 97--04, LIP - ENS Lyon, February 1997. [ bib \| .ps.Z \| Abstract ]
[59]	J.-C. Filliâtre. A decision procedure for Direct Predicate Calculus: study and implementation in the Coq system. Research Report 96--25, LIP - ENS Lyon, February 1995. [ bib \| .ps.Z \| Abstract ]
[60]	J.-C. Filliâtre. Une procédure de décision pour le Calcul des Prédicats Direct : étude et implémentation dans le système Coq. Rapport de DEA, Ecole Normale Supérieure, Juillet 1994. [ bib \| .dvi.gz ]
[61]	J. Courant et J.-C. Filliâtre. Formalisation de la théorie des langages formels en Coq. Rapport de maîtrise, Ecole Normale Supérieure, Septembre 1993. [ bib \| .dvi.gz ]

This file was generated by bibtex2html 1.97pl3.