Xinyu Feng

My research interests are in the area of programming languages and formal methods. In particular, I am interested in developing theories, programming languages and tools to build formally certified system software, with rigorous guarantees of safety and correctness.

Here is my CV and Research Statement.

PC Member:         TASE'09,     APLAS'08

On Programming Languages

1. Deny-Guarantee Reasoning.
   Mike Dodds, Xinyu Feng, Matthew Parkinson and Viktor Vafeiadis.
   Proc. 18th European Symposium on Programming (ESOP'09), York, UK, to appear, March 2009.
   
   
2. Local Rely-Guarantee Reasoning.
   Xinyu Feng.
   Proc. 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'09), Savannah, Georgia, USA, pages 315-327, January, 2009.
   
   Extended version: Technical Report TTIC-TR-2008-1, Toyota Technological Institute at Chicago, October 2008.
   
   
3. Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems.
   Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong.
   Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Toronto, Canada, pages 54-69, October 2008.
   
   
4. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. (presentation-ppt)
   Xinyu Feng, Zhong Shao, Yuan Dong and Yu Guo.
   Proc. 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), Tucson, Arizona, pages 170-182, June 2008
   
   Extended version: Technical Report YALEU/DCS/TR-1396
   
   
5. An Open Framework for Certified System Software.
   Xinyu Feng.
   Ph.D. Thesis, Yale University, December 2007
   
   
6. On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning. (presentation-ppt)
   Xinyu Feng, Rodrigo Ferreira, and Zhong Shao.
   Proc. 16th European Symposium on Programming (ESOP'07), Braga, Portugal, pages 173-188, March 2007.
   
   Extended version: Technical Report YALEU/DCS/TR-1374
   
   
7. An Open Framework for Foundational Proof-Carrying Code. (presentation-ppt)
   Xinyu Feng, Zhaozhong Ni, Zhong Shao, and Yu Guo.
   Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07), Nice, France, pages 67-78, January 2007.
   
   Extended version: Technical Report YALEU/DCS/TR-1373
   
   
8. Modular Verification of Assembly Code with Stack-Based Control Abstractions. (presentation-ppt)
   Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang and Zhaozhong Ni.
   Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006.
   
   Extended version: Technical Report YALEU/DCS/TR-1336
   
   
9. Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination. (presentation-ppt)
   Xinyu Feng and Zhong Shao.
   Proc. 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP'05), Tallinn, Estonia, pages 254-267, September 2005.
   
   Also see the poster presented at Cyber Trust 2005
   
   
10. Design of the Certifying Programming Language - Vero. (ps) (pdf)
    Xinyu Feng.
    Technical Report, Yale University, May 2004.

On Mobile Agent Systems

1. Mailbox-Based Scheme for Designing Mobile Agent Communication Protocols.
   Jiannong Cao, Xinyu Feng, Jian Lu, and Sajal K. Das.
   IEEE Computer, 35(9), pages 54-60, September 2002.
   
   
2. An Efficient Mailbox-Based Algorithm for Message Delivery in Mobile Agent Systems.
   Xinyu Feng, Jiannong Cao, Jian Lu, and Henry Chan.
   Proc. 5th International Conference on Mobile Agents (MA'01), Published in Lecture Notes in Computer Science, volume 2240, pages 135-151, Springer-Verlag, 2001.
   
   
3. Design and Analysis of Mobile Agent Communication Protocols. (pdf) (presentation-ppt)
   Xinyu Feng.
   Master thesis, Nanjing University, May 2002.

Also see my CV for a complete list.

ACM Digital Library      IEEE Xplore      Merriam-Webster Online      Programming Language Theory Text Online

The Coq Proof Assistant

more...