Claude Marché

64 papers A* 2A 1B 5C 6Journal 19Unranked 29

Year	Rank	Type	Title / Venue / Authors
2024	B	`conf`	Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. FMCAD Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft
2022	J	`jnl`	Automated formal analysis of temporal properties of Ladder programs. Int. J. Softw. Tools Technol. Transf. Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
2022	C	`conf`	Creusot: A Foundry for the Deductive Verification of Rust Programs. ICFEM Xavier Denis, Jacques-Henri Jourdan, Claude Marché
2022	J	`jnl`	The CoLiS platform for the analysis of maintainer scripts in Debian software packages. Int. J. Softw. Tools Technol. Transf. Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
2021	C	`conf`	Automated Verification of Temporal Properties of Ladder Programs. FMICS Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
2021	—	`conf`	Explaining Counterexamples with Giant-Step Assertion Checking. F-IDE@NFM Benedikt F. H. Becker, Cláudio Belo Lourenço, Claude Marché
2020	—	`conf`	Analysing installation scenarios of Debian packages. TACAS (2) Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
2020	J	`jnl`	Deductive verification with ghost monitors. Proc. ACM Program. Lang. Martin Clochard, Claude Marché, Andrei Paskevich
2019	—	`conf`	Ghost Code in Action: Automated Verification of a Symbolic Interpreter. VSTTE Benedikt F. H. Becker, Claude Marché
2018	J	`jnl`	Instrumenting a weakest precondition calculus for counterexample generation. J. Log. Algebraic Methods Program. Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy
2018	—	`conf`	Lightweight Interactive Proving inside an Automatic Program Verifier. F-IDE@FLoC Sylvain Dailler, Claude Marché, Yannick Moy
2017	J	`jnl`	A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. J. Formaliz. Reason. Ran Chen, Martin Clochard, Claude Marché
2017	—	`conf`	A Formally Verified Interpreter for a Shell-Like Programming Language. VSTTE Nicolas Jeannerod, Claude Marché, Ralf Treinen
2017	—	`conf`	Automating the Verification of Floating-Point Programs. VSTTE Clément Fumex, Claude Marché, Yannick Moy
2017	—	`conf`	How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. VSTTE Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
2016	B	`conf`	Counterexamples from Proof Failures in SPARK. SEFM David Hauzar, Claude Marché, Yannick Moy
2016	—	`conf`	Specification and Proof of High-Level Functional Properties of Bit-Level Programs. NFM Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché
2016	—	`conf`	Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. ISoLA (1) Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
2015	J	`jnl`	Bridging the Gap between Testing and Formal Verification in Ada Development. ERCIM News Claude Marché, Johannes Kanig
2015	J	`jnl`	Let's verify this with Why3. Int. J. Softw. Tools Technol. Transf. François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
2014	—	`conf`	Formalizing Semantics with an Automatic Program Verifier. VSTTE Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
2014	C	`conf`	The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. ABZ David Delahaye, Catherine Dubois, Claude Marché, David Mentré
2014	J	`jnl`	Verification of the functional behavior of a floating-point program: An industrial case study. Sci. Comput. Program. Claude Marché
2014	—	`conf`	Verified programs with binders. PLPV Martin Clochard, Claude Marché, Andrei Paskevich
2013	—	`conf`	Preserving User Proofs across Specification Changes. VSTTE François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
2012	—	`conf`	A Certified Multi-prover Verification Condition Generator. VSTTE Paolo Herms, Claude Marché, Benjamin Monate
2012	C	`conf`	Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. ABZ David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka
2011	J	`jnl`	Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. Math. Comput. Sci. Sylvie Boldo, Claude Marché
2011	—	`ed.`	Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers FoVeOOS Bernhard Beckert, Claude Marché
2011	B	`conf`	Hardware-Dependent Proofs of Numerical Programs. CPP Thi Minh Tuyen Nguyen, Claude Marché
2011	—	`conf`	The COST IC0701 Verification Competition 2011. FoVeOOS 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, Mattias Ulbrich
2010	—	`conf`	A Refinement Methodology for Object-Oriented Programs. FoVeOOS Asma Tafat, Sylvain Boulmé, Claude Marché
2010	J	`jnl`	Modular inference of subprogram contracts for safety checking. J. Symb. Comput. Yannick Moy, Claude Marché
2010	A	`conf`	Multi-Prover Verification of Floating-Point Programs. IJCAR Ali Ayad, Claude Marché
2010	—	`conf`	Specifying generic Java programs: two case studies. LDTA Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko
2008	J	`jnl`	Proving operational termination of membership equational programs. High. Order Symb. Comput. Francisco Durán, Salvador Lucas, Claude Marché, José Meseguer, Xavier Urbain
2007	—	`conf`	Jessie: an intermediate language for Java and C verification. PLPV Claude Marché
2007	—	`conf`	The Termination Competition. RTA Claude Marché, Hans Zantema
2007	A*	`conf`	The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. CAV Jean-Christophe Filliâtre, Claude Marché
2007	—	`conf`	Towards Modular Algebraic Specifications for Pointer Programs: A Case Study. Rewriting, Computation and Proof Claude Marché
2006	B	`conf`	Verification of JAVA CARD Applets Behavior with Respect to Transactions and Card Tears. SEFM Claude Marché, Nicolas Rousset
2005	B	`conf`	A case study of C source code verification: the Schorr-Waite algorithm. SEFM Thierry Hubert, Claude Marché
2005	J	`jnl`	Mechanically Proving Termination Using Polynomial Interpretations. J. Autom. Reason. Evelyne Contejean, Claude Marché, Ana Paula Tomás, Xavier Urbain
2005	J	`jnl`	Operational termination of conditional term rewriting systems. Inf. Process. Lett. Salvador Lucas, Claude Marché, José Meseguer
2005	—	`conf`	Reasoning About Java Programs with Aliasing and Frame Conditions. TPHOLs Claude Marché, Christine Paulin-Mohring
2004	—	`conf`	Formal Verification of a Commercial Smart Card Applet with Multiple Tools. AMAST Bart Jacobs, Claude Marché, Nicole Rauch
2004	J	`jnl`	Modular and incremental proofs of AC-termination. J. Symb. Comput. Claude Marché, Xavier Urbain
2004	C	`conf`	Multi-prover Verification of C Programs. ICFEM Jean-Christophe Filliâtre, Claude Marché
2004	C	`conf`	Proving termination of membership equational programs. PEPM Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, Xavier Urbain
2004	J	`jnl`	The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. J. Log. Algebraic Methods Program. Claude Marché, Christine Paulin-Mohring, Xavier Urbain
2002	J	`jnl`	Dam Failure Risk: Its Definition and Impact on Safety Assessment of Dam Structures. J. Decis. Syst. Claude Marché, Benoit Robert
2001	—	`ed.`	Constraints in Computational Logics: Theory and Applications, International Summer School, CCL'99 Gif-sur-Yvette, France, September 5-8, 1999, Revised Lectures CCL Hubert Comon, Claude Marché, Ralf Treinen
2000	—	`conf`	TALP: A Tool for the Termination Analysis of Logic Programs. RTA Enno Ohlebusch, Claus Claves, Claude Marché
1998	—	`conf`	Termination of Associative-Commutative Rewriting by Dependency Pairs. RTA Claude Marché, Xavier Urbain
1997	—	`conf`	Rewrite Systems for Natural, Integral, and Rational Arithmetic. RTA Evelyne Contejean, Claude Marché, Landy Rabehasaina
1996	—	`conf`	AC-Complete Unification and its Application to Theorem Proving. RTA Alexandre Boudet, Evelyne Contejean, Claude Marché
1996	—	`conf`	C RTA Evelyne Contejean, Claude Marché
1996	J	`jnl`	Normalized Rewriting: An Alternative to Rewriting Modulo a Set of Equations. J. Symb. Comput. Claude Marché
1994	A*	`conf`	Normalised Rewriting and Normalised Completion LICS Claude Marché
1993	—	`conf`	Normalized Rewriting - Application to Ground Completion and Standard Bases. Term Rewriting Claude Marché
1992	J	`jnl`	Termination and Completion Modulo Associativity, Commutativity and Identity. Theor. Comput. Sci. Jean-Pierre Jouannaud, Claude Marché
1992	J	`jnl`	The Word Problem of ACD-Ground Theories is Undecidable. Int. J. Found. Comput. Sci. Claude Marché
1991	—	`conf`	On Ground AC-Completion. RTA Claude Marché
1990	—	`conf`	Completion modulo Associativity, Commutativity and Identity (AC1). DISCO Jean-Pierre Jouannaud, Claude Marché