Here are all my publications

(sorted by date, from newest to oldest)

[1]

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. [ bib | .pdf ]

[2]

Claude Marché and Hans Zantema. The termination competition. In Franz Baader, editor, 18th International Conference on Rewriting Techniques and Applications (RTA'07), Lecture Notes in Computer Science, Paris, France, June 2007. Springer. [ bib ]

[3]

Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV'07), Braga, Portugal, March 2007. http://www.lri.fr/~marche/hubert07hav.pdf. [ bib ]

[4]

Yannick Moy and Claude Marché. Inferring local (non-)aliasing and strings for memory safety. In Heap Analysis and Verification (HAV'07), Braga, Portugal, March 2007. [ bib ]

[5]

Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 2007. [ bib ]

[6]

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 ]

[7]

Claude Marché. Towards modular algebraic specifications for pointer programs: a case study. In H. Comon-Lundh, C. Kirchner, and H. Kirchner, editors, Rewriting, Computation and Proof, volume 4600 of Lecture Notes in Computer Science, pages 235-258. Springer, 2007. [ bib ]

[8]

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 ]

[9]

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 ]

[10]

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 ]

[11]

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. Springer, August 2005. [ bib | .ps ]

[12]

Evelyne 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 | http ]

[13]

Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446-453, 2005. [ bib ]

[14]

Claude Marché. Preuves mécanisées de Propriétés de Programmes. Thèse d'habilitation, Université Paris 11, 2005. [ bib ]

[15]

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 ]

[16]

Evelyne Contejean, Claude Marché, and Xavier Urbain. CiME3, 2004. Available at http://cime.lri.fr/. [ bib | http ]

[17]

Evelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, 2004. [ bib | .ps.gz ]

[18]

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 ]

[19]

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 ]

[20]

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 ]

[21]

Claude Marché and Xavier Urbain. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation, 38:873-897, 2004. [ bib | http ]

[22]

Evelyne 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. http://cime.lri.fr. [ bib | http ]

[23]

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 ]

[24]

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 ]

[25]

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 ]

[26]

Hubert Comon, Claude Marché, and Ralf Treinen, editors. Constraints in Computational Logics, volume 2002 of Lecture Notes in Computer Science. Springer, 2001. [ bib ]

[27]

Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/. [ bib | http ]

[28]

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 ]

[29]

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 | .ps.gz | Abstract ]

[30]

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 | .ps.gz | Abstract ]

[31]

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 | .ps.gz | http | Abstract ]

[32]

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 | .ps.gz | Abstract ]

[33]

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 | .ps.gz | http | Abstract ]

[34]

Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253-288, 1996. [ bib | .ps.gz | Abstract ]

[35]

Claude Marché. Associative-commutative reduction orderings via head-preserving interpretations. Technical Report 95-2, LIFAC, E.N.S. de Cachan, January 1995. [ bib | .ps.gz | Abstract ]

[36]

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 | .ps.Z | Abstract ]

[37]

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 | .ps.gz | Abstract ]

[38]

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 | .ps.Z | Abstract ]

[39]

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 | .ps.Z | Abstract ]

[40]

Claude Marché. Normalized rewriting - application to ground completion and standard bases. Notes de cours de l'école de printemps, 1993. [ bib | .ps.Z | Abstract ]

[41]

Jean-Pierre Jouannaud and Claude Marché. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, 104:29-51, 1992. [ bib | .ps.Z | Abstract ]

[42]

Claude Marché. The word problem of ACD-ground theories is undecidable. International Journal of Foundations of Computer Science, 3(1):81-92, 1992. [ bib | .ps.Z | Abstract ]

[43]

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 ]

[44]

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 ]

[45]

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 ]

[46]

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 ]

[47]

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 ]

This file has been generated by bibtex2html 1.87.