Research

I am interested in programming languages and formal verification. I am a member of the PLaX group.

Here is my CV (2024-08).

Teaching

• Fall 2024. 22011510 / 081200D20: Formal Semantics of Programming Languages
• Fall 2024. 00399570: The Light of Science (Young Scholars) — Programming Language Pearls
• In the past
  • 22011510 / 081200D20: Formal Semantics of Programming Languages. Fall 2019. Fall 2020. Fall 2021. Fall 2022. Fall 2023.
  • 00399570: The Light of Science (Young Scholars) — Programming Language Pearls. Fall 2023.
  • 22011590 / 081200D19: Concurrency: Algorithms and Theories. Fall 2019. Fall 2020. Fall 2021. Fall 2022. Fall 2023.
  • 22011490: Compiler Design and Implementation (for ESE undergraduate students). Fall 2018.
  • 22010120: Compilers: Principles, Techniques, and Tools (for CS undergraduate students), with Xinyu Dai. Fall 2018.

Program committees: ESOP 2025, PLDI 2024, PriSC 2024, APLAS 2023, OOPSLA 2023, PriSC 2023, PaPoC 2022, PLDI 2022, CPP 2022, POPL 2022, ESOP 2021, CPP 2021, CPP 2020, APLAS 2019, POPL 2019, YR-CONCUR 2018, CoqPL 2017, CPP 2016

Publications

• Verifying Algorithmic Versions of the Lovász Local Lemma.
  Rongen Lin, Hongjin Liang and Xinyu Feng.
  To appear in Proc. 34th European Symposium on Programming (ESOP'25).
  [More...]
  
• A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model.
  Weijie Fan, Hongjin Liang, Xinyu Feng and Hanru Jiang.
  To appear in Proc. 34th European Symposium on Programming (ESOP'25).
  [More...]
  
• Verifying Optimizations of Concurrent Programs in the Promising Semantics.
  Junpeng Zha, Hongjin Liang, Xinyu Feng.
  In Proc. 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'22), San Diego, California, USA, pages 903-917, June 2022.
  [Paper] [@ACM] [More...]
  
• Abstraction for Conflict-Free Replicated Data Types.
  Hongjin Liang, Xinyu Feng.
  In Proc. 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21), Virtual, pages 636–650, June 2021.
  [Paper] [@ACM] [More...]
  
• Progress of Concurrent Objects.
  Hongjin Liang, Xinyu Feng.
  Foundations and Trends® in Programming Languages, Volume 5, Issue 4, pages 282-414, May 2020.
  (This is a tutorial for our work on formalizing and verifying progress of concurrent objects.)
  Also in the form of a book.
  [Paper] [@nowpublishers]
  
• Towards Certified Separate Compilation for Concurrent Programs.
  Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, Xinyu Feng.
  In Proc. 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'19), Phoenix, Arizona, USA, pages 111-125, June 2019. (Distinguished paper award)
  [Paper] [@ACM] [Video abstract] [More...]
  
• Progress of Concurrent Objects with Partial Methods.
  Hongjin Liang, Xinyu Feng.
  In Proc. 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'18), Los Angeles, California, USA, Article No. 20, January 2018.
  Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL, Article No. 20, January 2018.
  [Paper] [@ACM] [Technical report] [Slides (by Xinyu)]
  
• A Program Logic for Concurrent Objects under Fair Scheduling.
  Hongjin Liang, Xinyu Feng.
  In Proc. 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16), St. Petersburg, Florida, USA, pages 385-399, January 2016.
  [Paper] [@ACM] [Technical report] [Slides]
  
• Compositional Verification of Termination-Preserving Refinement of Concurrent Programs.
  Hongjin Liang, Xinyu Feng, Zhong Shao.
  In Proc. 23rd EACSL Annual Conference on Computer Science Logic and 29th Annual IEEE Symposium on Logic in Computer Science (CSL-LICS'14), Vienna, Austria, Article No. 65, July 2014.
  [Paper] [@ACM] [Technical report] [Slides]
  
• Refinement Verification of Concurrent Programs and Its Applications.
  Hongjin Liang.
  PhD Dissertation. May 2014.
  [English version] [Chinese version] [Defense slides]
• Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations.
  Hongjin Liang, Xinyu Feng, Ming Fu.
  ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 36, Issue 1, Article No. 3, March 2014.
  (This is a journal version of our POPL'12 paper.)
  [Paper] [@ACM]
  
• Characterizing Progress Properties of Concurrent Objects via Contextual Refinements.
  Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao.
  In Proc. 24th International Conference on Concurrency Theory (CONCUR'13), Buenos Aires, Argentina, pages 227-241, August 2013.
  [Paper] [@Springer] [Technical report] [Slides]
  
• Modular Verification of Linearizability with Non-Fixed Linearization Points.
  Hongjin Liang, Xinyu Feng.
  In Proc. 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13), Seattle, USA, pages 459-470, June 2013.
  [Paper] [@ACM] [Technical report] [Poster] [Slides]
  
• A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations.
  Hongjin Liang, Xinyu Feng, Ming Fu.
  In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12), Philadelphia, USA, pages 455-468, January 2012.
  [Paper] [@ACM] [Technical report] [Coq implementation] [Slides]
  
• A Pointer Logic Dealing with Uncertain Equality of Pointers.
  Hongjin Liang, Yu Zhang, Yiyun Chen, Zhaopeng Li, Baojian Hua.
  Journal of Software, 21(2):334-343, February 2010.
  [Paper (in Chinese)] [@JOS] [Appendix]
  

See also: DBLP