Project EVEREST, INRIA Sophia-Antipolis

yu DOT zhang AT sophia DOT inria DOT fr

Ph.D. (obtained in October 2005, at LSV, École Normale Supérieure de Cachan)

My research interests address essentially the formal methods and logical aspects of computer science. I am in particular interested in

  • formal information security, verification of cryptographic protocols
  • semantics of programming languages, type systems, category theory, automated reasoning
  • verification of embedded systems, program analysis

  • Papers

      Peer reviewed papers at international journals: 
  • Cryptographic Logical Relations.
    Theoretical Computer Science (to appear).

  •   Peer reviewed papers at international conferences: 
  • SystemC waiting-state automata.
    In VECoS'07, Algiers, Algeria, May 2007.
    Joint work with Bruno Monsuez and Franck Védrine.

  • On Completeness of Logical Relations for Monadic Types.
    In ASIAN'06, Tokyo, Japan, December 2006. (long version)
    Joint work with Slawomir Lasota and David Nowak.

  • Complete Lax Logical Relations for Cryptographic Lambda-Calculi.
    In CSL'2004, Karpacz, Poland, September 2004.
    Joint work with Jean Goubault-Larrecq, Slawomir Lasota and David Nowak.

  • Logical Relations for Dynamic Name Creation.
    In CSL/KGC 2003, Vienna, Austria, August 2003.
    Joint work with David Nowak.

  •   Ph.D. dissertation: 
  • Cryptographic Logical Relations
        --- What is the contextual equivalence for cryptographic protocols and how to prove it?
    ENS de Cachan, October 2005.
    Supervised by David Nowak and Jean Goubault-Larrecq.

  •   Others: 
  • Towards a static analysis of SystemC models.
    Research report DRT/LIST/DTSI/SOL/06-240, CEA Saclay, France, October 2006.
    Joint work with Franck Védrine.

  • This page is maintained by ZHANG Yu, last modified on August 8, 2007.