2010

Conférence Internationale avec comité de lecture

• [BRA10

  @inproceedings {
  	BRA10,
  	title	=	"{Formal Verification of Coalescing Graph-Coloring Register Allocation}",
  	author	=	" S. Blazy and and A. Appel ",
  	booktitle	=	"{ESOP'10, European Symposium On Programming, Paphos (Chypre)}",
  	year	=	2010,
  	month	=	"January",
  	series	=	"LNCS",
  	pages	=	"145-164",
  }

  ] S. Blazy , , A. Appel - Formal Verification of Coalescing Graph-Coloring Register Allocation, ESOP'10, European Symposium On Programming, Paphos (Chypre), January 2010, pp.145-164, Series LNCS,

2009

Revue Internationale avec comité de lecture

• [BL09

  @article {
  	BL09,
  	title	=	"{Mechanized semantics for the Clight subset of the C language}",
  	author	=	"S. Blazy and X. Leroy",
  	journal	=	"JAR, J. of Automated Reasoning",
  	year	=	2009,
  	volume	=	43,
  	number	=	3,
  	pages	=	"263-288",
  }

  ] S. Blazy , X. Leroy - Mechanized semantics for the Clight subset of the C language, JAR, J. of Automated Reasoning, vol. 43(3), pp. 263-288, 2009

Conférence Internationale avec comité de lecture

• [BR09

  @inproceedings {
  	BR09,
  	title	=	"{Live-Range Unsplitting for Faster Optimal Coalescing}",
  	author	=	" S. Blazy and ",
  	booktitle	=	"{LCTES'09 ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems}",
  	year	=	2009,
  	month	=	"January",
  	series	=	"ACM",
  	pages	=	"70-79",
  }

  ] S. Blazy , - Live-Range Unsplitting for Faster Optimal Coalescing, LCTES'09 ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, January 2009, pp.70-79, Series ACM,

Conférences invitées

• [BRS09

  @inproceedings {
  	BRS09,
  	title	=	"{Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe}",
  	author	=	" S. Blazy and and E. Soutif ",
  	year	=	2009,
  	month	=	"January",
  	note	=	"{Republication de l'article des JFLA 2008}",
  }

  ] S. Blazy , , E. Soutif - Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe, January 2009,

Rapport Scientifique

• [BRA09

  @techreport {
  	BRA09,
  	title	=	"{Formal Verification of Coalescing Graph-Coloring Register Allocation}",
  	author	=	"S. Blazy and and A. Appel",
  	number	=	"{CEDRIC-09-1832}",
  	institution	=	"{CEDRIC laboratory, CNAM-Paris, France}",
  	date	=	{01-01-2009},
  	pages	=	"32 pages",
  	note	=	"{note}",
  }

  ] S. Blazy , , A. Appel - Formal Verification of Coalescing Graph-Coloring Register Allocation, Date de dépot: 2009/01/01, Nb pages 32 pages, (Tech. Rep.: CEDRIC-09-1832)

2008

Revue Internationale avec comité de lecture

• [LB08a

  @article {
  	LB08a,
  	title	=	"{Formal verification of a C-like memory model and its uses for verifying program transformations}",
  	author	=	"X. Leroy and S. Blazy",
  	journal	=	"JAR, J. of Automated Reasoning",
  	year	=	2008,
  	volume	=	41,
  	number	=	1,
  	pages	=	"1-31",
  }

  ] X. Leroy , S. Blazy - Formal verification of a C-like memory model and its uses for verifying program transformations, JAR, J. of Automated Reasoning, vol. 41(1), pp. 1-31, 2008

Conférence Nationale avec comité de lecture

• [BRS08a

  @inproceedings {
  	BRS08a,
  	title	=	"{Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe}",
  	author	=	" S. Blazy and and E. Soutif ",
  	booktitle	=	"{JFLA'08 Journées Francophones des Langages Applicatifs}",
  	year	=	2008,
  	month	=	"January",
  	pages	=	"31-46",
  	note	=	"{Cette publication a fait l'objet d'une invitation aux 1ères Journées Nationales du GDR GPL, du 28 au 30 Janvier 2009, à Toulouse (France), où elle a été présentée de nouveau.}",
  }

  ] S. Blazy , , E. Soutif - Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe, JFLA'08 Journées Francophones des Langages Applicatifs, January 2008, pp.31-46,
• [BRS08

  @inproceedings {
  	BRS08,
  	title	=	"{Coloration avec préférences : complexité, inégalités valides et vérification formelle}",
  	author	=	" S. Blazy and and E. Soutif ",
  	booktitle	=	"{ROADEF'08, Clermont-Ferrand, 25-27 Février}",
  	year	=	2008,
  	month	=	"January",
  	pages	=	"123-138",
  }

  ] S. Blazy , , E. Soutif - Coloration avec préférences : complexité, inégalités valides et vérification formelle, ROADEF'08, Clermont-Ferrand, 25-27 Février, January 2008, pp.123-138,

Directions d'ouvrages scientifiques

• [BLA08

  @book {
  	BLA08,
  	title	=	"{Actes de la conférence JFLA2008}",
  	author	=	"S. Blazy",
  	year	=	2008,
  	publisher	=	"INRIA",
  }

  ] S. Blazy - Actes de la conférence JFLA2008, January 2008, INRIA,

Mémoire de HDR

• [Bla08a

  @misc {
  	Bla08a,
  	title	=	"{Sémantiques formelles}",
  	author	=	"S. Blazy",
  	year	=	2008,
  	pages	=	"138 pages",
  	address	=	"{CEDRIC Laboratory, Paris, France}",
  	note	=	"{Post-Doctoral Degree (Phd students supervisor) Directeur: Rapporteur 1: Rapporteur 2: Membre du jury: Membre du jury: Membre du jury:}",
  }

  ] S. Blazy - Sémantiques formelles, Soutenue le: 23 October 2008, pp. 138 pages,

Rapport Scientifique

• [BR08a

  @techreport {
  	BR08a,
  	title	=	"{Live-Range Unsplitting for Faster Optimal Coalescing (extended version)}",
  	author	=	"S. Blazy and ",
  	number	=	"{CEDRIC-08-1609}",
  	institution	=	"{CEDRIC laboratory, CNAM-Paris, France}",
  	date	=	{01-01-2008},
  }

  ] S. Blazy , - Live-Range Unsplitting for Faster Optimal Coalescing (extended version), Date de dépot: 2008/01/01, (Tech. Rep.: CEDRIC-08-1609)

2007

Revue Nationale avec comité de lecture

• [BLA07

  @article {
  	BLA07,
  	title	=	"{Comment gagner confiance en C ?}",
  	author	=	"S. Blazy",
  	journal	=	"TSI, Technique et Science Informatiques",
  	year	=	2007,
  	volume	=	26,
  	number	=	9,
  	pages	=	"1195-2000",
  }

  ] S. Blazy - Comment gagner confiance en C ?, TSI, Technique et Science Informatiques, vol. 26(9), pp. 1195-2000, 2007

Conférence Internationale avec comité de lecture

• [BLA07a

  @inproceedings {
  	BLA07a,
  	title	=	"{Experiments in validating formal semantics for C}",
  	author	=	" S. Blazy ",
  	booktitle	=	"{C/C++ Verification Workshop, Oxford, United Kingdom}",
  	year	=	2007,
  	month	=	"January",
  	series	=	"ICIS-R07015",
  	pages	=	"95-102",
  }

  ] S. Blazy - Experiments in validating formal semantics for C, C/C++ Verification Workshop, Oxford, United Kingdom, January 2007, pp.95-102, Series ICIS-R07015,
• [WB07

  @inproceedings {
  	WB07,
  	title	=	"{Separation Logic for Small-step Cminor}",
  	author	=	" A. W. Appel and S. Blazy ",
  	booktitle	=	"{TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany)}",
  	year	=	2007,
  	month	=	"January",
  	series	=	"LNCS 4732",
  	pages	=	"5-21",
  }

  ] A. W. Appel , S. Blazy - Separation Logic for Small-step Cminor, TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), January 2007, pp.5-21, Series LNCS 4732,

Conférence Nationale avec comité de lecture

• [BRS07

  @inproceedings {
  	BRS07,
  	title	=	"{Coloration avec préférences dans les graphes triangulés}",
  	author	=	" S. Blazy and and E. Soutif ",
  	booktitle	=	"{Journées Graphes et Algorithmes, Paris}",
  	year	=	2007,
  	month	=	"January",
  	pages	=	"32",
  	note	=	"{note}",
  }

  ] S. Blazy , , E. Soutif - Coloration avec préférences dans les graphes triangulés, Journées Graphes et Algorithmes, Paris, January 2007, pp.32,

Rapport Scientifique

• [AB07

  @techreport {
  	AB07,
  	title	=	"{Separation logic for small-step Cminor (extended version)}",
  	author	=	"A. Appel and S. Blazy",
  	number	=	"{CEDRIC-07-1358}",
  	institution	=	"{CEDRIC laboratory, CNAM-Paris, France}",
  	date	=	{01-01-2007},
  	pages	=	"29 pages",
  }

  ] A. Appel , S. Blazy - Separation logic for small-step Cminor (extended version), Date de dépot: 2007/01/01, Nb pages 29 pages, (Tech. Rep.: CEDRIC-07-1358)

2006

Conférence Internationale avec comité de lecture

• [BLD06

  @inproceedings {
  	BLD06,
  	title	=	"{Formal verification of a C compiler front-end}",
  	author	=	" S. Blazy and X. Leroy and Z. Dargaye ",
  	booktitle	=	"{FM'06: 14th Symposium on Formal Methods, Hamilton, Canada}",
  	year	=	2006,
  	month	=	"January",
  	series	=	"LNCS",
  	volume	=	4085,
  	pages	=	"460-475",
  }

  ] S. Blazy , X. Leroy , Z. Dargaye - Formal verification of a C compiler front-end, FM'06: 14th Symposium on Formal Methods, Hamilton, Canada, January 2006, Vol. 4085, pp.460-475, Series LNCS,

2005

Conférence Internationale avec comité de lecture

• [BL05

  @inproceedings {
  	BL05,
  	title	=	"{Formal verification of a memory model for C-like imperative languages}",
  	author	=	" S. Blazy and X. Leroy ",
  	booktitle	=	"{ICFEM'05, Int. Conf on Formal Engineering Methods, Manchester, UK}",
  	year	=	2005,
  	month	=	"January",
  	series	=	"LNCS",
  	volume	=	3785,
  	pages	=	"280-299",
  }

  ] S. Blazy , X. Leroy - Formal verification of a memory model for C-like imperative languages, ICFEM'05, Int. Conf on Formal Engineering Methods, Manchester, UK, January 2005, Vol. 3785, pp.280-299, Series LNCS,

2003

Conférence Internationale avec comité de lecture

• [BGL03

  @inproceedings {
  	BGL03,
  	title	=	"{Reuse of Specification Patterns with the B Method}",
  	author	=	" S. Blazy and F. Gervais and R. Laleau ",
  	booktitle	=	"{ZB 2003: Formal Specification and Development in Z and B, Turku, Finland}",
  	year	=	2003,
  	month	=	"January",
  	series	=	"LNCS",
  	volume	=	2651,
  	pages	=	"40-57",
  	note	=	"{3rd International Conference of B and Z Users.}",
  }

  ] S. Blazy , F. Gervais , R. Laleau - Reuse of Specification Patterns with the B Method, ZB 2003: Formal Specification and Development in Z and B, Turku, Finland, January 2003, Vol. 2651, pp.40-57, Series LNCS,

Conférence Nationale avec comité de lecture

• [BGL03a

  @inproceedings {
  	BGL03a,
  	title	=	"{Une démarche outillée pour spécifier formellement des patrons de conception réutilisables}",
  	author	=	" S. Blazy and F. Gervais and R. Laleau ",
  	booktitle	=	"{Objets, Composants et Modèles dans l'ingénierie des SI}",
  	year	=	2003,
  	month	=	"January",
  	note	=	"{Workshop associé à INFORSID'2003, Nancy, 3 juin 2003.}",
  }

  ] S. Blazy , F. Gervais , R. Laleau - Une démarche outillée pour spécifier formellement des patrons de conception réutilisables, Objets, Composants et Modèles dans l'ingénierie des SI, January 2003,

2002

Rapport Scientifique

• [BGL02

  @techreport {
  	BGL02,
  	title	=	"{Un exemple de réutilisation de patterns de spécification avec la méthode B}",
  	author	=	"S. Blazy and F. Gervais and R. Laleau",
  	number	=	"{CEDRIC-02-395}",
  	institution	=	"{CEDRIC laboratory, CNAM-Paris, France}",
  	date	=	{01-01-2002},
  }

  ] S. Blazy , F. Gervais , R. Laleau - Un exemple de réutilisation de patterns de spécification avec la méthode B, Date de dépot: 2002/01/01, (Tech. Rep.: CEDRIC-02-395)
• [BLA02

  @techreport {
  	BLA02,
  	title	=	"{Transformations certifiées de programmes impératifs}",
  	author	=	"S. Blazy",
  	number	=	"{CEDRIC-02-398}",
  	institution	=	"{CEDRIC laboratory, CNAM-Paris, France}",
  	date	=	{01-01-2002},
  }

  ] S. Blazy - Transformations certifiées de programmes impératifs, Date de dépot: 2002/01/01, (Tech. Rep.: CEDRIC-02-398)

2000

Revue Internationale avec comité de lecture

• [BLA00

  @article {
  	BLA00,
  	title	=	"{Specifying and Automatically Generating a Specialization Tool for Fortran 90}",
  	author	=	"S. Blazy",
  	journal	=	"Journal on Automated Software Engineerin",
  	year	=	2000,
  	volume	=	7,
  	number	=	4,
  	pages	=	"345-376",
  }

  ] S. Blazy - Specifying and Automatically Generating a Specialization Tool for Fortran 90, Journal on Automated Software Engineerin, vol. 7(4), pp. 345-376, 2000

Conférence Internationale avec comité de lecture

• [BBM00

  @inproceedings {
  	BBM00,
  	title	=	"{An automatic detection of prokaryotic CoDing Sequences Combining Several Independent Methods}",
  	author	=	" S. Bocs and S. Blazy and C. M�digue and P. Glaser ",
  	booktitle	=	"{Genome 2000, Paris}",
  	year	=	2000,
  	month	=	"January",
  	note	=	"{note}",
  }

  ] S. Bocs , S. Blazy , C. M�digue , P. Glaser - An automatic detection of prokaryotic CoDing Sequences Combining Several Independent Methods, Genome 2000, Paris, January 2000,

1998

Revue Internationale avec comité de lecture

• [BF98

  @article {
  	BF98,
  	title	=	"{Partial evaluation for program comprehension}",
  	author	=	"S. Blazy and P. Facon",
  	journal	=	"Symposium on Partial Evaluation",
  	year	=	1998,
  	volume	=	30,
  	number	=	3,
  	note	=	"{note}",
  }

  ] S. Blazy , P. Facon - Partial evaluation for program comprehension, Symposium on Partial Evaluation, vol. 30(3), 1998

1997

Conférence Internationale avec comité de lecture

• [BF97

  @inproceedings {
  	BF97,
  	title	=	"{Application of formal methods to the development of a software maintenance tool}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{IEEE Conf. on Automated Software Engineering, Lake Tahoe}",
  	year	=	1997,
  	month	=	"January",
  	pages	=	"162-171",
  }

  ] S. Blazy , P. Facon - Application of formal methods to the development of a software maintenance tool, IEEE Conf. on Automated Software Engineering, Lake Tahoe, January 1997, pp.162-171,

1996

Conférence Internationale avec comité de lecture

• [BF96

  @inproceedings {
  	BF96,
  	title	=	"{Interprocedural analysis for program comprehension by specialization}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{4th IEEE Workshop on Program Comprehension, Berlin}",
  	year	=	1996,
  	month	=	"January",
  	pages	=	"133-141",
  }

  ] S. Blazy , P. Facon - Interprocedural analysis for program comprehension by specialization, 4th IEEE Workshop on Program Comprehension, Berlin, January 1996, pp.133-141,
• [BF96a

  @inproceedings {
  	BF96a,
  	title	=	"{An automatic interprocedural analysis for the understanding of scientific application programs}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{Seminar on partial evaluation, Dagsthul castle}",
  	year	=	1996,
  	month	=	"January",
  	series	=	"LNCS 1110",
  	pages	=	"1-16",
  }

  ] S. Blazy , P. Facon - An automatic interprocedural analysis for the understanding of scientific application programs, Seminar on partial evaluation, Dagsthul castle, January 1996, pp.1-16, Series LNCS 1110,

1995

Conférence Internationale avec comité de lecture

• [BF95

  @inproceedings {
  	BF95,
  	title	=	"{Formal specification and prorotyping of a program specializer}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{TAPSOFT'95, Aarhus}",
  	year	=	1995,
  	month	=	"January",
  	series	=	"LNCS 915",
  	pages	=	"666-680",
  }

  ] S. Blazy , P. Facon - Formal specification and prorotyping of a program specializer, TAPSOFT'95, Aarhus, January 1995, pp.666-680, Series LNCS 915,

1994

Revue Internationale avec comité de lecture

• [BF94a

  @article {
  	BF94a,
  	title	=	"{Partial evaluation for the understanding of Fortran programs}",
  	author	=	"S. Blazy and P. Facon",
  	journal	=	"IJSEKE, Int. J. of Software Engineering and Knowledge Engineering",
  	year	=	1994,
  	volume	=	4,
  	number	=	4,
  	pages	=	"535-559",
  	note	=	"{December 1994, International Journal of Software Engineering and Knowledge Engineering}",
  }

  ] S. Blazy , P. Facon - Partial evaluation for the understanding of Fortran programs, IJSEKE, Int. J. of Software Engineering and Knowledge Engineering, vol. 4(4), pp. 535-559, 1994

Conférence Internationale avec comité de lecture

• [BF94

  @inproceedings {
  	BF94,
  	title	=	"{SFAC: a tool for program comprehension by specialization}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{3rd IEEE Workshop on Program Comprehension, Washington D.C., 14-15 December}",
  	year	=	1994,
  	month	=	"December",
  	pages	=	"162-167",
  }

  ] S. Blazy , P. Facon - SFAC: a tool for program comprehension by specialization, 3rd IEEE Workshop on Program Comprehension, Washington D.C., 14-15 December, December 1994, pp.162-167,

1993

Conférence Internationale avec comité de lecture

• [BF93

  @inproceedings {
  	BF93,
  	title	=	"{Partial evaluation as an aid to the comprehension of Fortran programs}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{2nd IEEE Workshop on Program Comprehension, Capri, Italy}",
  	year	=	1993,
  	month	=	"January",
  	pages	=	"46-54",
  }

  ] S. Blazy , P. Facon - Partial evaluation as an aid to the comprehension of Fortran programs, 2nd IEEE Workshop on Program Comprehension, Capri, Italy, January 1993, pp.46-54,
• [BF93a

  @inproceedings {
  	BF93a,
  	title	=	"{Partial evaluation for the understanding of Fortran programs}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{Soft. Eng. and Knowledge Eng. (SEKE), San Francisco}",
  	year	=	1993,
  	month	=	"January",
  	pages	=	"517-525",
  }

  ] S. Blazy , P. Facon - Partial evaluation for the understanding of Fortran programs, Soft. Eng. and Knowledge Eng. (SEKE), San Francisco, January 1993, pp.517-525,
• [BF93b

  @inproceedings {
  	BF93b,
  	title	=	"{Partial evaluation and symbolic computation for the understanding of Fortran programs}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{CAISE'93, Paris, France}",
  	year	=	1993,
  	month	=	"January",
  	series	=	"LNCS 685",
  	pages	=	"184-198",
  }

  ] S. Blazy , P. Facon - Partial evaluation and symbolic computation for the understanding of Fortran programs, CAISE'93, Paris, France, January 1993, pp.184-198, Series LNCS 685,

1992

Conférence Internationale avec comité de lecture

• [BF92

  @inproceedings {
  	BF92,
  	title	=	"{Evaluation partielle pour la compréhension de programmes Fortran}",
  	author	=	" S. Blazy and P. Facon ",
  	booktitle	=	"{Software Engineering and its applications, Toulouse, December}",
  	year	=	1992,
  	month	=	"December",
  	pages	=	"411-417",
  }

  ] S. Blazy , P. Facon - Evaluation partielle pour la compréhension de programmes Fortran, Software Engineering and its applications, Toulouse, December, December 1992, pp.411-417,
• [HVM92

  @inproceedings {
  	HVM92,
  	title	=	"{Software maintenance: an analysis of industrial needs and constraints}",
  	author	=	" M. Haziza and J. Voidrot and E. Minor and L. Pofelski and S. Blazy ",
  	booktitle	=	"{IEEE Conf. on Software Maintenance, Orlando}",
  	year	=	1992,
  	month	=	"January",
  	pages	=	"18-26",
  }

  ] M. Haziza , J. Voidrot , E. Minor , L. Pofelski , S. Blazy - Software maintenance: an analysis of industrial needs and constraints, IEEE Conf. on Software Maintenance, Orlando, January 1992, pp.18-26,