Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications : Claude Marché

Back
marche
[79] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.73. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.73 edition, July 2012. https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf. [ bib ]
[78] David Mentré, Claude Marché, Jean-Christophe Filliâtre, and Masashi Asuka. Discharging proof obligations from Atelier B using multiple automated provers. In Steve Reeves and Elvinia Riccobene, editors, ABZ'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Lecture Notes in Computer Science, Pisa, Italy, June 2012. Springer. http://hal.inria.fr/hal-00681781/en/. [ bib | full paper on HAL ]
We present a method to discharge proof obligations from Atelier B using multiple SMT solvers. It is based on a faithful modeling of B's set theory into polymorphic first-order logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged.

[77] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.72. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.72 edition, May 2012. https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf. [ bib ]
[76] Paolo Herms, Claude Marché, and Benjamin Monate. A certified multi-prover verification condition generator. In Rajeev Joshi, Peter Müller, and Andreas Podelski, editors, VSTTE, Lecture Notes in Computer Science. Springer, 2012. [ bib | .pdf ]
[75] Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, Radu Grigore, Marieke Huisman, Vladimir Klebanov, Claude Marché, Rosemary Monahan, Wojciech Mostowski, Nadia Polikarpova, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, and Mattias Ulbrich. The COST IC0701 verification competition 2011. In Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, Lecture Notes in Computer Science. Springer, 2012. [ bib | .pdf ]
[74] Thi Minh Tuyen Nguyen and Claude Marché. Hardware-dependent proofs of numerical programs. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, Lecture Notes in Computer Science. Springer, December 2011. [ bib ]
[73] François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. The Why3 platform, version 0.71. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.71 edition, October 2011. https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf. [ bib ]
[72] 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 paper on HAL ]
[71] 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, pages 53-64, Wroclaw, Poland, August 2011. [ bib | .pdf ]
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

[70] K. 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 paper on HAL ]
[69] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, February 2011. http://why3.lri.fr/. [ bib ]
[68] Yannick Moy and Claude Marché. The Jessie plugin for Deduction Verification in Frama-C - Tutorial and Reference Manual. INRIA & LRI, 2011. http://krakatoa.lri.fr/. [ bib | PDF | http ]
[67] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science, pages 153-167. Springer, January 2011. [ bib ]
[66] Romain Bardou and Claude Marché. Perle de preuve: les tableaux creux. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib ]
[65] Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 5:377-393, 2011. [ bib | DOI | .pdf ]
[64] 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 paper on HAL ]
[63] 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 paper on HAL ]
[62] Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of Lecture Notes in Artificial Intelligence, pages 127-141, Edinburgh, Scotland, July 2010. Springer. [ bib | .pdf ]
[61] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, pages 143-159, Paris, France, June 2010. http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083. [ bib ]
[60] Yannick Moy and Claude Marché. Jessie Plugin, Boron version. INRIA, 2010. http://frama-c.com/jessie/jessie-tutorial.pdf. [ bib | PDF | .pdf ]
[59] Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement approach for correct-by-construction object-oriented programs. Technical Report 7310, INRIA, 2010. [ bib | full paper on HAL ]
[58] Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Specifying generic Java programs: two case studies. In Claus Brabrand and Pierre-Etienne Moreau, editors, Tenth Workshop on Language Descriptions, Tools and Applications. ACM Press, 2010. [ bib | full paper on HAL ]
[57] Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 45:1184-1211, 2010. [ bib | DOI | full paper on HAL ]
[56] 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 paper on HAL ]
[55] 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 | PDF | .html ]
[54] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[53] Elena Tushkanova, Alain Giorgetti, Claude Marché, and Olga Kouchnarenko. Modular specification of Java programs. Technical Report 7097, INRIA, 2009. [ bib | full paper 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.

[52] Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseo publications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf. [ bib | .pdf ]
[51] Claude Marché. The Krakatoa tool for deductive verification of Java programs. Winter School on Object-Oriented Verification, Viinistu, Estonia, January 2009. http://krakatoa.lri.fr/ws/. [ bib | PDF | http ]
[50] Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1-2):59-88, 2008. [ bib | PDF | .pdf ]
[49] Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language, 2008. http://frama-c.cea.fr/acsl.html. [ bib | PDF | .html ]
[48] Yannick Moy and Claude Marché. Jessie Plugin Tutorial, Lithium version. INRIA, 2008. http://www.frama-c.cea.fr/jessie.html. [ bib | PDF | .html ]
[47] 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, volume 4590 of Lecture Notes in Computer Science, pages 173-177, Berlin, Germany, July 2007. Springer. [ bib | PDF | .pdf ]
[46] Claude Marché and Hans Zantema. The termination competition. In Franz Baader, editor, 18th International Conference on Rewriting Techniques and Applications (RTA'07), volume 4533 of Lecture Notes in Computer Science, pages 303-313, Paris, France, June 2007. Springer. [ bib | Slides | PDF | .pdf ]
[45] Claude Marché, Hans Zantema, and Johannes Waldmann. The termination competition 2007. In Dieter Hofbauer and Alexander Serebrenik, editors, Extended Abstracts of the 9th International Workshop on Termination, WST'07, June 2007. http://www.lri.fr/~marche/termination-competition/. [ bib | http ]
[44] Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV'07), pages 81-93, Braga, Portugal, March 2007. [ bib | PDF | .pdf ]
[43] Yannick Moy and Claude Marché. Inferring local (non-)aliasing and strings for memory safety. In Heap Analysis and Verification (HAV'07), pages 35-51, Braga, Portugal, March 2007. [ bib | PDF | .pdf ]
[42] Claude Marché. Towards modular algebraic specifications for pointer programs: a case study. In Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 235-258. Springer, 2007. [ bib ]
[41] Claude Marché. Jessie: an intermediate language for Java and C verification. In Programming Languages meets Program Verification (PLPV), pages 1-2, Freiburg, Germany, 2007. ACM. [ bib | DOI | http ]
[40] Claude Marché and Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. In Dang Van Hung and Paritosh Pandya, editors, 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, September 2006. IEEE Comp. Soc. Press. [ bib | .ps ]
[39] Claude Marché and Hans Zantema. The termination competition 2006. In Alfons Geser and Harald Sondergaard, editors, Extended Abstracts of the 8th International Workshop on Termination, WST'06, August 2006. http://www.lri.fr/~marche/termination-competition/. [ bib | http ]
[38] Claude Marché. Preuves mécanisées de Propriétés de Programmes. Thèse d'habilitation, Université Paris 11, December 2005. [ bib | .pdf ]
[37] Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September 2005. IEEE Comp. Soc. Press. [ bib | .ps ]
[36] Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 179-194. Springer, August 2005. [ bib | .ps ]
[35] 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 ]
[34] Évelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning, 34(4):325-363, 2005. [ bib | DOI | Abstract ]
[33] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446-453, 2005. [ bib ]
We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs

[32] Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving termination of membership equational programs. In ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, Verona, Italy, August 2004. ACM Press. [ bib ]
[31] Bart Jacobs, Claude Marché, and Nicole Rauch. Formal verification of a commercial smart card applet with multiple tools. In Algebraic Methodology and Software Technology, volume 3116 of Lecture Notes in Computer Science, Stirling, UK, July 2004. Springer. [ bib ]
[30] É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 ]
[29] Jean-Christophe Filliâtre and Claude Marché. Multi-prover verification of C programs. In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, 6th International Conference on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 15-29, Seattle, WA, USA, November 2004. Springer. [ bib | .ps.gz ]
[28] Claude Marché and Xavier Urbain. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation, 38:873-897, 2004. [ bib | http ]
[27] Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1-2):89-106, 2004. http://krakatoa.lri.fr. [ bib | http | .ps ]
[26] Néstor Cataño, Marek Gawkowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain. Logical techniques for applet verification. Deliverable 5.2, IST VerifiCard Project, 2003. http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf. [ bib | .pdf ]
[25] Évelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. Proving termination of rewriting with cime. In Albert Rubio, editor, Extended Abstracts of the 6th International Workshop on Termination, WST'03, pages 71-73, June 2003. Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain. [ bib | http ]
[24] Enno Ohlebusch, Claus Claves, and Claude Marché. The talp tool for termination analysis of logic programs. In Albert Rubio, editor, Extended Abstracts of the 6th International Workshop on Termination, WST'03, June 2003. http://bibiserv.techfak.uni-bielefeld.de/talp/. [ bib | http ]
[23] Néstor Cataño, M. Gawlowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain. Logical techniques for applet verification. Deliverable 5.2, IST VerifiCard project, 2003. http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf. [ bib | .pdf ]
[22] Keiichirou Kusakari, Claude Marché, and Xavier Urbain. Termination of associative-commutative rewriting using dependency pairs criteria. Research Report 1304, LRI, 2002. http://www.lri.fr/~urbain/textes/rr1304.ps.gz. [ bib | .ps.gz ]
[21] Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/. [ bib | http ]
[20] Enno Ohlebusch, Claus Claves, and Claude Marché. TALP: A tool for the termination analysis of logic programs. In Leo Bachmair, editor, 11th International Conference on Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 270-273, Norwich, UK, July 2000. Springer. Available at http://bibiserv.techfak.uni-bielefeld.de/talp/. [ bib | http ]
[19] Claude Marché. Normalized Rewriting: an unified view of Knuth-Bendix completion and Gröbner bases computation. Progress in Computer Science and Applied Logic, 15:193-208, 1998. [ bib | PDF | Abstract ]
[18] Claude Marché and Xavier Urbain. Termination of associative-commutative rewriting by dependency pairs. In Tobias Nipkow, editor, 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 241-255, Tsukuba, Japan, April 1998. Springer. [ bib | PDF | Abstract ]
[17] Evelyne Contejean, Claude Marché, and Landy Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. In Hubert Comon, editor, 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 98-112, Barcelona, Spain, June 1997. Springer. [ bib | DOI | PDF | Abstract ]
[16] Alexandre Boudet, Evelyne Contejean, and Claude Marché. AC-complete unification and its application to theorem proving. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 18-32, New Brunswick, NJ, USA, July 1996. Springer. [ bib | DOI | PDF | Abstract ]
[15] Evelyne Contejean and Claude Marché. CiME: Completion Modulo E. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 416-419, New Brunswick, NJ, USA, July 1996. Springer. System Description available at http://cime.lri.fr/. [ bib | DOI | PDF | http | Abstract ]
[14] Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253-288, 1996. [ bib | PDF | Abstract ]
[13] Claude Marché. Associative-commutative reduction orderings via head-preserving interpretations. Technical Report 95-2, LIFAC, E.N.S. de Cachan, January 1995. [ bib | PDF | Abstract ]
[12] Claude Marché. Normalized rewriting - application to ground completion and standard bases. In Hubert Comon and Jean-Pierre Jouannaud, editors, Term Rewriting, volume 909 of Lecture Notes in Computer Science, pages 154-169. French Spring School of Theoretical Computer Science, Springer, 1995. [ bib | PDF | Abstract ]
[11] Claude Marché. Normalized Rewriting: an unified view of Knuth-Bendix completion and Gröbner bases computation. In Manuel Bronstein and Volker Weispfenning, editors, Proceedings of the Conference on Symbolic Rewriting Techniques, Monte Verita, Switzerland, 1995. [ bib | PDF | Abstract ]
[10] Claude Marché. Normalised rewriting and normalised completion. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 394-403, Paris, France, July 1994. IEEE Comp. Soc. Press. [ bib | PDF | Abstract ]
[9] Claude Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certaines classes de théories équationnelles. Thèse de doctorat, Université Paris-Sud, Orsay, France, October 1993. [ bib | PDF | Abstract ]
[8] Claude Marché. Normalized rewriting - application to ground completion and standard bases. Notes de cours de l'école de printemps, 1993. [ bib | PDF | Abstract ]
[7] Jean-Pierre Jouannaud and Claude Marché. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, 104:29-51, 1992. [ bib | PDF | Abstract ]
[6] Claude Marché. The word problem of ACD-ground theories is undecidable. International Journal of Foundations of Computer Science, 3(1):81-92, 1992. [ bib | PDF | Abstract ]
[5] Claude Marché. The word problem of ACD-ground theories is undecidable. Research Report 663, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, April 1991. [ bib ]
[4] Claude Marché. On ground AC-completion. In Ronald. V. Book, editor, 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, Como, Italy, April 1991. Springer. [ bib ]
[3] Claude Marché. On AC-termination and ground AC-completion. Research Report 598, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, October 1990. [ bib ]
[2] Jean-Pierre Jouannaud and Claude Marché. Completion modulo associativity, commutativity and identity. In Alfonso Miola, editor, Proc. Int. Symposium on Design and Implementation of Symbolic Computation Systems, LNCS 429, pages 111-120, Capri, Italy, April 1990. Springer. [ bib ]
[1] Claude Marché. Complétion modulo associativité, commutativité et élément neutre. Research Report 513, Laboratoire de Recherche en Informatique, Université de Paris-Sud, Orsay, France, September 1989. [ bib ]

Back
This page was generated by bibtex2html.