1月20日至23日，第43届编程语言原理国际会议（简称POPL）在美国佛罗里达州圣彼德斯堡召开。中国科学技术大学特任副研究员梁红瑾和教授冯新宇在并发程序验证领域取得新进展，首次设计出一种验证并发对象无饥饿性与无死锁性的程序逻辑，该研究成果发表在第43届POPL上。
多处理器系统上的并发程序在执行时，有多个线程同时共享系统资源。当对共享资源的管理和使用不当时，常常会出现饥饿、死锁、活锁等活性问题，造成一个或多个线程无限期等待资源而不再响应。由于并发系统自身的复杂性，程序测试难以找出全部问题。梁红瑾等提出了一个新的程序逻辑，能够严格证明一个并发系统不可能出现饥饿、死锁、活锁等问题。研究人员将并发环境的各种行为分为两类，称为“阻塞”和“延迟”，饥饿、死锁等问题分别对应于这两类并发环境的不同组合。然后，针对阻塞与延迟，分别设计出特定的程序规范和推理规则，保证并发系统最终一定会响应并有所进展。这样得到的程序逻辑具有很好的通用性，可定制为对各个单一性质的验证。该程序逻辑已应用于一些经典并发算法验证，例如，该工作在国际上首次形式化验证了锁耦合链表算法的无饥饿性，以及乐观链表算法和惰性链表算法的无死锁性等。该研究成果为验证实际并发程序的无饥饿性、无死锁性等活性性质提供了理论基础。
POPL是讨论编程语言和编程系统最新突破的主要论坛，内容涵盖编程语言的理论、编程语言的设计、编译器技术、程序分析、程序验证、可信软件等众多研究领域。该论文是本年度唯一来自中国大陆研究机构的论文。此前，中国大陆研究机构作为第一署名单位仅在POPL上发表过3篇论文，其中第一篇便是由梁红瑾、冯新宇课题组在第39届POPL会议上发表的。
该研究工作得到国家自然科学基金的资助。