Παρακολούθηση
Claude Marché
Claude Marché
Senior Research Scientist, Inria
Η διεύθυνση ηλεκτρονικού ταχυδρομείου έχει επαληθευτεί στον τομέα inria.fr - Αρχική σελίδα
Τίτλος
Παρατίθεται από
Παρατίθεται από
Έτος
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification: (Tool Paper)
JC Filliâtre, C Marché
International Conference on Computer Aided Verification, 173-177, 2007
5132007
Why3: Shepherd your herd of provers
F Bobot, JC Filliâtre, C Marché, A Paskevich
Boogie 2011: First International Workshop on Intermediate Verification …, 2011
4122011
ACSL: ANSI/ISO C Specification Language, version 1.4, 2009
P Baudin, JC Filliâtre, C Marché, B Monate, Y Moy, V Prevosto
345*
Multi-prover verification of C programs
JC Filliâtre, C Marché
Formal Methods and Software Engineering: 6th International Conference on …, 2004
3072004
The Krakatoa tool for certification of Java/JavaCard programs annotated in JML
C Marché, C Paulin-Mohring, X Urbain
The Journal of Logic and Algebraic Programming 58 (1), 89-106, 2004
2682004
Mechanically proving termination using polynomial interpretations
E Contejean, C Marché, AP Tomás, X Urbain
Journal of Automated Reasoning 34 (4), 325-363, 2005
1192005
Operational termination of conditional term rewriting systems
S Lucas, C Marché, J Meseguer
Information Processing Letters 95 (4), 446-453, 2005
1122005
Normalized rewriting: an alternative to rewriting modulo a set of equations
C Marché
Journal of symbolic computation 21 (3), 253-288, 1996
1121996
Proving operational termination of membership equational programs
F Durán, S Lucas, C Marché, J Meseguer, X Urbain
Higher-Order and Symbolic Computation 21 (1), 59-88, 2008
1012008
Let’s verify this with Why3
F Bobot, JC Filliâtre, C Marché, A Paskevich
International Journal on Software Tools for Technology Transfer 17, 709-727, 2015
872015
Multi-prover verification of floating-point programs
A Ayad, C Marché
International Joint Conference on Automated Reasoning, 127-141, 2010
852010
Discharging proof obligations from Atelier B using multiple automated provers
D Mentré, C Marché, JC Filliâtre, M Asuka
International Conference on Abstract State Machines, Alloy, B, VDM, and Z …, 2012
682012
Proving termination of membership equational programs
F Durán, S Lucas, J Meseguer, C Marché, X Urbain
Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and …, 2004
652004
CiME: Completion modulo E
E Contejean, C Marché
International Conference on Rewriting Techniques and Applications, 416-419, 1996
621996
Separation Analysis for Weakest Precondition-based Verification
T Hubert, C Marché
HAV 2007-Heap Analysis and Verication, 81--93, 2007
602007
Creusot: A Foundry for the Deductive Verification of Rust Programs
X Denis, JH Jourdan, C Marché
International Conference on Formal Engineering Methods, 90-105, 2022
592022
A case study of C source code verification: the Schorr-Waite algorithm
T Hubert, C Marché
Third IEEE International Conference on Software Engineering and Formal …, 2005
592005
Normalised rewriting and normalised completion
C Marché
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 394-403, 1994
591994
ACSL: ANSI/ISO C Specification Language, version 1.4
P Baudin, JC Filliâtre, C Marché, B Monate, Y Moy, V Prevosto
CEA, http://frama-c. com/download/acsl_1 6, 2009
582009
The termination competition
C Marché, H Zantema
International Conference on Rewriting Techniques and Applications, 303-313, 2007
572007
Δεν είναι δυνατή η εκτέλεση της ενέργειας από το σύστημα αυτή τη στιγμή. Προσπαθήστε ξανά αργότερα.
Άρθρα 1–20