Xinyu Feng  (冯新宇)

Professor
Department of Computer Science and Technology
Nanjing University


Contact:
163 Xianlin Road
Department of Computer Science and Technology
Nanjing University
Nanjing, Jiangsu 210023, China
       
Phone:
Fax:
Email:
 
+86-512-87161319
+86-512-87161319
xyfeng AT nju DOT edu DOT cn



News and Events

  1. Welcome to SETTA 2018!

  2. Paper to appear at INFOCOM 2018: POMP: Protocol Oblivious SDN Programming with Automatic Multi-Table Pipelining.

  3. Paper@POPL 2018: Progress of Concurrent Objects with Partial Methods.

Research

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.


Teaching

  1. Spring, 2017. 011167, Foundations of Programming Languages
  2. Spring, 2017. CS05115, Theories of Programming Languages
  3. Spring, 2016. 011167, Foundations of Programming Languages
  4. Spring, 2016. CS05115, Theories of Programming Languages
  5. Spring, 2015. 011167, Foundations of Programming Languages
  6. Spring, 2015. CS05115, Theories of Programming Languages
  7. Spring, 2014. 011167, Foundations of Programming Languages
  8. Fall, 2013. CS05115, Theories of Programming Languages
  9. Spring, 2013. 011167, Foundations of Programming Languages
  10. Fall, 2012. CS05115, Theories of Programming Languages
  11. Summer, 2012. 011M0701, Frontier of Research on High-Confidence Software
  12. Fall, 2011. CS05115, Theories of Programming Languages

Professional Activities
SETTA'18,     CoqPL'18,     POPL'18,     APLAS'17,     FMAC'17,     SETTA'17,     ESOP'17,     SETTA'16,     APLAS'15,     WWV'15,     ICPP'15,     ITP'15,     ICALP'15,     POPL'15 (ERC),     TASE'14,     LOLA'13,     POPL'13,     CPP'12,     ICTAC'12,     TASE'12,     2012 Open64 Workshop,     APLAS'11,     LOLA'11,     TASE'09,     APLAS'08

Selected Publications
  1. POMP: Protocol Oblivious SDN Programming with Automatic Multi-Table Pipelining
    Chunhui He and Xinyu Feng.
    Proc. 2018 IEEE Conference on Computer Communications (INFOCOM'18), to appear, Honolulu, HI, USA. April 2018. © IEEE.


  2. Progress of Concurrent Objects with Partial Methods (TR, and POPL talk)
    Hongjin Liang and Xinyu Feng.
    Proc. 45th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'18), article 20, Los Angeles, CA, USA, January 2018. © ACM.
    Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. January 2018. © ACM.


  3. A Practical Verification Framework for Preemptive OS Kernels (TR, CAV Talk by Ming Fu, and project page)
    Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li.
    Proc. 28th International Conference on Computer Aided Verification (CAV'16), part II, pages 59--79, Toronto, ON, Canada, July 17-23, 2016. © Springer.


  4. A Program Logic for Concurrent Objects under Fair Scheduling (TR, and POPL talk by Hongjin Liang)
    Hongjin Liang and Xinyu Feng.
    Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16), pages 385-399, St. Petersburg, FL, USA, January 2016. © ACM.


  5. Compositional Verification of Termination-Preserving Refinement of Concurrent Programs (TR, and Talk by Hongjin Liang)
    Hongjin Liang, Xinyu Feng and Zhong Shao.
    Proc. Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS'14), pages 65:1-65:10, Vienna, Austria, July 2014. © ACM.


  6. Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations
    Hongjin Liang, Xinyu Feng and Ming Fu. (Journal version of POPL'12)
    ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 36, No. 1, Article 3, March 2014. © ACM.

  7. Characterizing Progress Properties of Concurrent Objects via Contextual Refinements (TR, and Talk by Hongjin Liang)
    Hongjin Liang, Jan Hoffmann, Xinyu Feng and Zhong Shao.
    Proc. 24th International Conference on Concurrency Theory (CONCUR'13), Buenos Aires, Argentina, pages 227--241, August 2013. © Springer.

  8. Modular Verification of Linearizability with Non-Fixed Linearization Points (TR, Poster, and Talk by Hongjin Liang )
    Hongjin Liang and Xinyu Feng.
    Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13), Seattle, WA, USA, pages 459-470, June, 2013. © ACM.

  9. A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations (TR, Talk by Hongjin Liang, and Coq Implementation)
    Hongjin Liang, Xinyu Feng, and Ming Fu.
    Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12), Philadelphia, Pennsylvania, USA, pages 455-468, January, 2012. © ACM.

  10. 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. © Spring.

  11. 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. © Springer.

  12. 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.

  13. Deny-Guarantee Reasoning.
    Mike Dodds, Xinyu Feng, Matthew Parkinson and Viktor Vafeiadis.
    Proc. 18th European Symposium on Programming (ESOP'09), York, UK, pages 363-377, March 2009. © Springer.

  14. 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. © ACM.

    Extended version: Technical Report TTIC-TR-2008-1, Toyota Technological Institute at Chicago, October 2008.

  15. 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.

  16. 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. (Superceded by the journal version)

    Extended version: Technical Report YALEU/DCS/TR-1396

  17. An Open Framework for Certified System Software.
    Xinyu Feng.
    Ph.D. Thesis, Yale University, December 2007

  18. 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

  19. 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

  20. 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

  21. 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

  22. See a complete list at DBLP



Xinyu Feng
Last modified: Sun Dec 31, 2017