[47] Benedikt Becker, Jean-Christophe Filliâtre, and Claude Marché. Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup. Technical report, Université Paris-Saclay, January 2020. [ bib | full text on HAL ]
[46] Nicolas Jeannerod, Yann Régis-Gianas, Claude Marché, Mihaela Sighireanu, and Ralf Treinen. Specification of UNIX utilities. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ]
[45] Benedikt Becker, Claude Marché, Nicolas Jeannerod, and Ralf Treinen. Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ]
[44] Léo Andrès. Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification. Rapport de stage de M1, Université Paris Sud, August 2019. [ bib | full text on HAL ]
[43] Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, and Gidon Ernst. Verifythis 2018: A program verification competition. Research report, Université Paris-Saclay, January 2019. [ bib | full text on HAL ]
[42] Martin Clochard, Andrei Paskevich, and Claude Marché. Deductive verification via ghost debugging. Research Report 9219, Inria, 2018. [ bib | full text on HAL ]
[41] Lucas Baudin. Deductive verification with the help of abstract interpretation. Technical report, Univ Paris-Sud, November 2017. [ bib | full text on HAL ]
[40] Ilham Dami and Claude Marché. The CoLiS language: syntax, semantics and associated tools. Technical Report 0491, Inria, October 2017. [ bib | full text on HAL ]
[39] Clément Fumex, Claude Marché, and Yannick Moy. Automated verification of floating-point computations in Ada programs. Research Report RR-9060, Inria, April 2017. [ bib | full text on HAL ]
[38] Ran Chen, Martin Clochard, and Claude Marché. A formal proof of a Unix path resolution algorithm. Research Report RR-8987, Inria, December 2016. [ bib | full text on HAL ]
[37] David Hauzar, Claude Marché, and Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. Research Report RR-8854, Inria Saclay Ile-de-France, February 2016. [ bib | full text on HAL ]
[36] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. A pragmatic type system for deductive verification. Research report, Université Paris Sud, 2016. https://hal.archives-ouvertes.fr/hal-01256434v3. [ bib | full text on HAL ]
In the context of deductive verication, it is customary today to handle programs with pointers using either separation logic, dynamic frames, or explicit memory models. Yet we can observe that in numerous programs, a large amount of code ts within the scope of Hoare logic, provided we can statically control aliasing. When this is the case, the code correctness can be reduced to simpler verication conditions which do not require any explicit memory model. This makes verication conditions more amenable both to automated theorem proving and to manual inspection and debugging. In this paper, we devise a method of such static aliasing control for a programming language featuring nested data structures with mutable components. Our solution is based on a type system with singleton regions and eects, which we prove to be sound.

[35] Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Research Report 8821, Inria, December 2015. [ bib | full text on HAL ]
[34] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Fast parallel graph-search with splittable and catenable frontiers. Technical report, Inria, January 2015. [ bib | full text on HAL ]
[33] Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. Research Report 1560, LRI, June 2013. [ bib | full text on HAL | http | .pdf ]
[32] Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie De Quatrebarbes, and Stéphane Laurent. Médiation scientifique : une facette de nos métiers de la recherche. Interne, Inria, March 2013. [ bib | full text on HAL | http ]
Dans ce monde devenu numérique nous savons que c'est une de nos missions d'acteur de la recherche publique, que de rendre accessibles les sciences du numérique au plus grand nombre. Ceci afin que chaque citoyenne et citoyen maîtrise, au delà des usages, les principaux fondements de cette mutation numérique. Et nous croyons que c'est l'acquisition d'une culture scientifique sur ces sujets qui est le levier de cette appropriation. C'est notre mission et notre plaisir d'y contribuer. Ce document a pour but d'aider chaque collègue Inria intéressé à participer à ce volet de nos missions. Devenue une facette de notre métier, comme le rappelle le Plan Stratégique Inria [1], ce que nous appelons médiation scientifique en sciences du numérique (alias, " mecsci ") se professionnalise et change d'échelle. Et c'est environ 1 % de nos ressources qui a vocation à y être consacré. Pour tout l'institut on parle donc de près de 40 équivalents temps-plein distribués à travers le travail quotidien ou ponctuel de plusieurs centaines de collègues chercheurs, ingénieurs, communicants, etc.. Une telle énergie mérite d'être bien employée : au service des meilleurs objectifs ; vers des cibles bien définies qui ont de vrais besoins sur ces sujets ; dans le cadre d'actions leviers qui aident à faire bouger les choses ; et avec une méthodologie efficace qui optimise ce que nous investissons dans de telles activités ; tout en respectant et en encourageant les dynamiques locales et individuelles indépendantes qui restent les sources vives de la médiation scientifique. Voilà pourquoi il y a juste besoin d'offrir en partage à chacune et chacun les éléments fondateurs et méthodologiques de cette médiation scientifique. Offrir aussi quelques bonnes pratiques très concrètes. On parle donc ici d'une organisation distribuée d'actions collaboratives d'où émerge le service public de popularisation scientifique visé. C'est ce que ce document se propose de décrire ici.

Keywords: médiation scientifique ; culture scientifique ; recherche ; popularisation des sciences ; service public.
[31] Claude Marché and Asma Tafat. Weakest precondition calculus, revisited using Why3. Research Report RR-8185, INRIA, December 2012. [ bib | full text on HAL | .pdf ]
[30] Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Reasoning with triggers. Research Report RR-7986, INRIA, June 2012. [ bib | full text on HAL | .pdf ]
SMT solvers can decide the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism.

Keywords: Quantifiers, Triggers, SMT Solvers, Theories
[29] Jasmin C. Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. Technical report, Tech. Univ. Munich, 2012. http://www21.in.tum.de/~blanchet/tff1spec.pdf. [ bib | .pdf ]
[28] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: Mathematics and program. Research Report 7826, INRIA, December 2011. [ bib | full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.

Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis
[27] Asma Tafat and Claude Marché. Binary heaps formally verified in Why3. Research Report 7780, INRIA, October 2011. http://hal.inria.fr/inria-00636083/en/. [ bib | full text on HAL ]
Keywords: Why3
[26] Krishnamani Kalyanasundaram and Claude Marché. Automated generation of loop invariants using predicate abstraction. Research Report 7714, INRIA, August 2011. http://hal.inria.fr/inria-00615623/en/. [ bib | full text on HAL ]
[25] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. Technical Report 2044, Cédric laboratory, CNAM Paris, France, 2011. [ bib | .pdf | Abstract ]
[24] Thi Minh Tuyen Nguyen and Claude Marché. Proving floating-point numerical programs by analysis of their assembly code. Research Report 7655, INRIA, 2011. http://hal.inria.fr/inria-00602266/en/. [ bib | full text on HAL ]
[23] Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. Research Report 7793, INRIA, 2011. http://hal.inria.fr/hal-00639977/en/. [ bib | full text on HAL ]
[22] Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. Research Report 1538, LRI, Université Paris Sud, December 2010. [ bib | PDF | .pdf | Abstract ]
[21] Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform (version 2). Technical Report 7128, INRIA, 2010. http://hal.inria.fr/inria-00439232/en/. [ bib | full text on HAL ]
[20] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement approach for correct-by-construction object-oriented programs. Technical Report 7310, INRIA, 2010. [ bib | full text on HAL ]
[19] Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Research Report 7412, INRIA, 2010. http://hal.inria.fr/inria-00525384/en/. [ bib | full text on HAL ]
[18] Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. Technical Report 7128, INRIA, 2009. http://hal.inria.fr/inria-00439232. [ bib | full text on HAL ]
[17] Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Modular specification of Java programs. Technical Report 7097, INRIA, 2009. [ bib | full text on HAL ]
This work investigates the question of modular specification of generic Java classes and methods. The first part introduces a specification language for Java programs. In the second part the language is used to specify an array sorting algorithm by selection. The third and the fourth parts define a syntax proposal for the specification a generic Java programs, through two examples. The former is the specification of the generic method for sorting arrays which comes in the java.util.Arrays class of the Java API. The latter is the specification of the java.util.HashMap class and its use for memoization.

[16] Ali Ayad. On formal methods for certifying floating-point C programs. Research Report 6927, INRIA, 2009. [ bib | full text on HAL ]
[15] Guillaume Melquiond and Sylvain Pion. Directed rounding arithmetic operations. Technical Report 2899, ISO C++ Standardization Committee, 2009. [ bib ]
[14] Jean-François Couchot, Alain Giorgetti, and Nicolas Stouls. Graph-based Reduction of Program Verification Conditions. Research Report 6702, INRIA Saclay -- Île-de-France, October 2008. [ bib | full text on HAL ]
[13] Évelyne Contejean, Julien Forest, and Xavier Urbain. Deep-Embedded Unification. Research Report 1547, Cédric laboratory, CNAM Paris, France, 2008. [ bib ]
[12] Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq - version 2. Description of a Coq contribution, Université Paris Sud, December 2007. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ]
[11] Yannick Moy. Checking C pointer programs for memory safety. Research Report 6334, INRIA, October 2007. [ bib | PDF | .pdf ]
[10] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Certification of automated termination proofs. Research Report 1185, CEDRIC, May 2007. [ bib ]
[9] Louis Mandel and Luc Maranget. Programming in JoCaml -- extended version. Technical Report 6261, INRIA, 2007. [ bib | PDF | .pdf ]
[8] Louis Mandel. Prototype of AADL simulation in SCADE. ASSERT deliverable 4.3.2-2, ASSERT Project, November 2006. [ bib ]
[7] Julien Signoles. Towards a ML extension with Refinement: a Semantic Issue. Technical Report 1440, LRI, University of Paris Sud, March 2006. [ bib | .pdf ]
[6] Louis Mandel. Report on modeling GALS in SCADE. ASSERT deliverable 4.3.2-1, ASSERT Project, February 2006. [ bib ]
[5] Jean-Christophe Filliâtre. Backtracking iterators. Research Report 1428, LRI, Université Paris Sud, January 2006. [ bib | .ps.gz ]
[4] Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq. Description of a Coq contribution, Université Paris Sud, January 2006. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ]
[3] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Research Report DSIC II/01/05, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, February 2005. [ bib ]
[2] Vikrant Chaudhary. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML : A case study. Technical report, IIT internship report, July 2004. [ bib ]
[1] Évelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, 2004. [ bib | .ps.gz ]