Accéder directement au contenu

Sandrine Blazy

12
Documents
Identifiants chercheurs

Présentation

Publications

1002
Image document

Mechanized semantics for the Clight subset of the C language

Sandrine Blazy , Xavier Leroy
Journal of Automated Reasoning, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩
Article dans une revue inria-00352524v1
Image document

Formal verification of a C-like memory model and its uses for verifying program transformations

Xavier Leroy , Sandrine Blazy
Journal of Automated Reasoning, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩
Article dans une revue inria-00289542v1
Image document

Comment gagner confiance en C ?

Sandrine Blazy
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2007, numéro spécial "Langages applicatifs", 26 (9), pp.1195-1200. ⟨10.3166/TSI.26.1195-1200⟩
Article dans une revue inria-00292049v1
Image document

Register allocation by graph coloring under full live-range splitting

Sandrine Blazy , Benoît Robillard
ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded systems (LCTES'2009), ACM, Jun 2009, Dublin, Ireland
Communication dans un congrès inria-00387749v1

Which C semantics to embed in the front-end of a formally verified compiler?

Sandrine Blazy
TTVSI (Tools and Techniques for Verification of System Infrastructure), Mar 2008, Oxford, United Kingdom. pp.31
Communication dans un congrès inria-00292441v1
Image document

Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe

Sandrine Blazy , Benoît Robillard , Eric Soutif
JFLA (Journées Francophones des Langages Applicatifs), INRIA, Jan 2008, Etretat, France. pp.31-46
Communication dans un congrès inria-00202713v1
Image document

Coloration avec préférences : complexité, inégalités valides et vérification formelle

Benoît Robillard , Sandrine Blazy , Eric Soutif
ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, ROADEF, Feb 2008, Clermont-Ferrand, France. pp.123-138
Communication dans un congrès inria-00260712v1
Image document

Separation Logic for Small-step Cminor

Andrew W. W. Appel , Sandrine Blazy
20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. pp.5-21
Communication dans un congrès inria-00165915v1

Coloration avec préférences dans les graphes triangulés

Sandrine Blazy , Benoît Robillard , Eric Soutif
Journées Graphes et algorithmes (JGA'07), Nov 2007, Paris, France. pp.32
Communication dans un congrès inria-00292045v1
Image document

Experiments in validating formal semantics for C

Sandrine Blazy
C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102
Communication dans un congrès inria-00292043v1
Image document

Formal Verification of a C Compiler Front-end

Sandrine Blazy , Zaynah Dargaye , Xavier Leroy
FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩
Communication dans un congrès inria-00106401v1
Image document

Formal verification of a memory model for C-like imperative languages

Sandrine Blazy , Xavier Leroy
ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. pp.280-299, ⟨10.1007/11576280⟩
Communication dans un congrès inria-00077921v1