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.
A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations
Hongjin Liang, Xinyu Feng, and Ming Fu.
Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12), Philadelphia, USA, to appear, January, 2012.
Weak Updates and Separation Logic
Gang Tan, Zhong Shao, Xinyu Feng, and Hongxu Cai.
New Generation Comput. 29(1): 3-29, 2011 © 2011 Springer-Verlag.
Reasoning about Optimistic Concurrency Using a Program Logic for History
Ming Fu, Yong Li, Xinyu Feng, Zhong Shao and Yu Zhang.
Proc. 21st International Conference on Concurrency Theory (CONCUR'10),
Paris, France, pages 388-402, August 2010.
Parameterized Memory Models and Concurrent Separation Logic
Rodrigo Ferreira, Xinyu Feng and Zhong Shao.
Proc. 19th European Symposium on Programming (ESOP'10), Paphos, Cyprus, pages 267-286, March 2010.
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.
Xinyu Feng, Zhong Shao, Yu Guo, and Yuan Dong.
Journal of Automated Reasoning (Special Issue on Operating System Verification),
42 (2-4): 301-347, April 2009.
© Springer Science + Business Media B.V.2009.
Mike Dodds, Xinyu Feng, Matthew Parkinson and Viktor Vafeiadis.
Proc. 18th European Symposium on Programming (ESOP'09),
York, UK, pages 363-377, March 2009.
Local Rely-Guarantee Reasoning.
Proc. 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'09),
Savannah, Georgia, USA, pages 315-327, January, 2009.
Technical Report TTIC-TR-2008-1,
Toyota Technological Institute at Chicago, October 2008.
- more ...