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).
  
  
• 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).
  
  
• Verified Validation for Affine Scheduling in Polyhedral Compilation.
  Xuyang Li, Hongjin Liang, and Xinyu Feng.
  In Proc. 18th International Symposium on Theoretical Aspects of Software Engineering (TASE'24), Guiyang, China, pages 287–305, July 2024.
  
  
• Verifying Optimizations of Concurrent Programs in the Promising Semantics.
  Junpeng Zha, Hongjin Liang and 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.
  
  
• Abstraction for Conflict-Free Replicated Data Types.
  Hongjin Liang and Xinyu Feng.
  In Proc. 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21), Virtual, pages 636–650, June 2021.
  
  
• Progress of Concurrent Objects.
  Hongjin Liang and 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 @nowpublishers.
  
  
• Towards Certified Separate Compilation for Concurrent Programs.
  Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha and 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