Lilian Burdy

I am senior research associate in the Everest project.

My current research activities concern program verification. More precisely, my main interests are:

Specification languages

Weakest precondition calculus

Automatic proofing

Recent CV

From October 2000 until July 2003, I was research architect in the Gemplus Research Labs.

I did my PhD in collaboration between the CEDRIC Lab ( CNAM Paris) and Matra Transport International (now Siemens Transportation Systems): Expression dépourvuees de sens de la théorie des ensembles: Application à la méthode B.

Publications

• L. Burdy, M. Pavlova
  Java Bytecode Specification and Validation
  To appear in SAC 06, Dijon, France, April 2006.
  
• R. Sola, S. Coudert, S. Gabriele, S. Hoffmann, L. Burdy
  Microkernel API formal modelisation
  SAME 2005 Forum, Nice, France, October 2005.
  
• M. Pavlova, G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet
  Enforcing high-level security properties for applets
  In P. Paradinas and J.-J. Quisquater, editors, Proceedings of CARDIS'04, Toulouse, France, August 2004. Kluwer Academic Publishers.
  [pdf]
• L. Burdy, A. Requet, J.-L. Lanet.
  Java Applet Correctness: a Developer-Oriented Approach
  FME 2003: Formal Methods, LNCS 2805, p 422-439, Springer-Verlag, Pisa, September 2003
  [ps]
• L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino and E. Poll
  An overview of JML tools and applications
  FMICS'03, volume 80 of ENTCS, Elsevier, Trondheim, 2003
  [ps] [pdf]
• L. Burdy, A. Requet.
  Extending B with control flow breaks
  ZB 2003: Formal Specification and Development in Z and B, LNCS 2651, p 513-527, Springer-Verlag, Turku, 2003
  [ps] [pdf]
• L. Burdy; L. Casset, A. Requet.
  Développement d’un vérifieur de byte-code embarqué
  Technique et Science Informatiques (TSI), 22, 2003
  [ps] [pdf]
• L. Burdy, A. Requet.
  JACK : Java Applet Correctness Kit
  4th Gemplus Developer Conference, Singapore, November 2002
  [pdf]
• L. Casset, L. Burdy, A. Requet.
  Formal development of an embedded bytecode verifier
  International Conference on Dependable Systems & Networks (DSN '02), pp. 51-58, IEEE Press, Washington D.C., 2002
  [pdf]
• L. Burdy.
  B vs. Coq to prove a Garbage Collector
  TPHOLs 2001: Supplemental Proceedings - in Technical Report EDI-INF-RR-0046
  [pdf]
• L. Burdy, J.-M. Meynadier.
  Experience on the Use of a Formal Method in a Railway Company
  9th IFAC Symposium on Control in Transportation System - Braunschweig - 2000
• L. Burdy, J.-M. Meynadier
  Automatic refinement
  FM'99 workshop -- Applying B in an industrial context : Tools, Lessons and Techniques - Toulouse - 1999
  [pdf]
• P. Behm, L. Burdy, J.-M. Meynadier
  Well Defined B
  B'98: Recent Advances in the Development and Use of the B Method, Second International B Conference, LNCS 1393, p 29-45, Montpellier, April 1998
• L. Burdy
  A treatment of partiality : its application to the B method
  Workshop on mechanization of partial function CADE 15 - Lindau 1998
  [ps]
• L. Burdy
  Obligation de preuve de raffinement en B
  1ère conférence B - Nantes 1996

Invited speaker

• Preuve d'un vérifieur de byte code JavaCard: métriques et retour d'expérience
  Journées B: présentation des outils universitaires sur B, exposés sur le B Evénementiel, preuves avec B et la balbulette. 13-14 juin 2002. CNAM. Paris
  [ps] [pdf]
• From Formal Specification to an Implementation of an Embedded Verifier for Java Card
  Séminaire QSL du Pôle ``Intelligence Logicielle'' La Méthode B 28 février 2002 LORIA
  [ppt]

Tutorial

• Design by Contract and Increased Dependability of Java applications with JML
  with Joe Kiniry and Erik Poll
  FM 05, University of Newcastle upon Tyne, UK, July 2005

Program comittees

• B 2007 Conference
• AFADL 2006 Conference
• CASSIS 04 Workshop
• ZB 2003 Conference

Research Projects

• GECCOO