• Programming languages design and implementation, language-based security, certifying compilers.
• Formal methods, specification and verification, applications of advanced type systems.

Dachuan Yu joined DoCoMo USA Labs in 2004. He received a Ph.D. in Computer Science from Yale University in 2004 and an M.E. in Computer Software from Nanjing University in 1999.

• Dynamic Test Input Generation for Web Applications
  Gary Wassermann, Dachuan Yu, Ajay Chander, Dinakar Dhurjati, Hiroshi Inamura, and Zhendong Su.
  2008 International Symposium on Software Testing and Analysis (ISSTA'08), Seattle, WA, July 2008, © ACM 2008.
• Better Abstractions for Secure Server-Side Scripting
  Dachuan Yu, Ajay Chander, Hiroshi Inamura, and Igor Serikov.
  17th International World Wide Web Conference (WWW'08), Beijing, China, April 2008, © ACM 2008.
  Extended version available as Technical Report DCL-TR-2007-0035, DoCoMo USA Labs, July 2007.
• More Typed Assembly Languages for Confidentiality
  Dachuan Yu.
  5th Asian Symposium on Programming Languages and Systems (APLAS'07), Singapore, November 2007, © Springer-Verlag 2007.
  Extended version available as Technical Report DCL-TR-2006-0021, DoCoMo USA Labs, September 2006.
• Using XCAP to Certify Realistic System Code: Machine Context Management
  Zhaozhong Ni, Dachuan Yu, and Zhong Shao.
  20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'07), Kaiserslautern, Germany, September 2007. LNCS Vol. 4732, © Springer-Verlag 2007.
• JavaScript Instrumentation for Browser Security
  Dachuan Yu, Ajay Chander, Nayeem Islam, and Igor Serikov.
  34th ACM Symposium on Principles of Programming Languages (POPL'07), Nice, France, January 2007, © ACM 2007.
• Variance and Generalized Constraints for C# Generics
  Burak Emir, Andrew Kennedy, Claudio Russo, and Dachuan Yu.
  20th European Conference on Object-Oriented Programming (ECOOP'06), Nantes, France, July 2006. LNCS Vol. 4067, © Springer-Verlag 2006.
• A Typed Assembly Language for Confidentiality
  Dachuan Yu and Nayeem Islam.
  2006 European Symposium on Programming (ESOP'06), Vienna, Austria, March 2006. LNCS Vol. 3924, © Springer-Verlag 2006.
  Extended version available as Technical Report DCL-TR-2005-0002, DoCoMo USA Labs, San Jose, CA, March 2005.
• Safety Verification of Low-Level Code
  Dachuan Yu.
  PhD thesis,Yale University, New Haven, CT, December 2004.
• Verification of Safety Properties for Concurrent Assembly Code
  Dachuan Yu and Zhong Shao.
  2004 ACM International Conference on Functional Programming (ICFP'04), Snowbird, Utah, September 2004, © ACM 2004.
• Building Certified Libraries for PCC: Dynamic Storage Allocation (Extended Version)
  Dachuan Yu, Nadeem A. Hamid, and Zhong Shao.
  Science of Computer Programming (SCP), Volume 50, Issues 1-3, Pages 101-127, March 2004, © Elsevier 2004.
• Formalization of Generics for the .NET Common Language Runtime
  Dachuan Yu, Andrew Kennedy, and Don Syme.
  31st ACM Symposium on Principles of Programming Languages (POPL'04), Venice, Italy, January 2004, © ACM 2004.
• Building Certified Libraries for PCC: Dynamic Storage Allocation
  Dachuan Yu, Nadeem A. Hamid, and Zhong Shao.
  2003 European Symposium on Programming (ESOP'03), Warsaw, Poland, April 2003. LNCS Vol. 2618, © Springer-Verlag 2003.
• Supporting Binary Compatibility with Static Compilation
  Dachuan Yu, Zhong Shao, and Valery Trifonov.
  2nd USENIX Java[TM] Virtual Machine Research and Technology Symposium (JVM'02), San Francisco, California, August 2002, © USENIX 2002.
  Winner of the Best Student Paper Award.
• Type-Preserving Compilation of Featherweight IL
  Dachuan Yu, Valery Trifonov, and Zhong Shao.
  Workshop on Formal Techniques for Java-like Programs (FTfJP'02), Málaga, Spain, June 2002.
• An Encoding of Fomega in LF
  Carsten Schürmann, Dachuan Yu, and Zhaozhong Ni.
  Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'01), Siena, Italy, June 2001. ENTCS Vol. 58.1, © Elsevier 2001.