Title:     Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification

　　Speaker:   贺飞 清华大学

　　Time:      7月1日（周四）10:00am

　　Venue:    中科院软件园区5号楼334房间，计算机科学国家重点实验室报告厅

　　Abstract:  Analyzing multi-threaded programs is hard due to the number of thread interleavings. Partial orders can be used for modeling and analyzing multi-threaded programs. However, there is no dedicated decision procedure for solving partial order constraints. In this paper, we propose a novel ordering consistency theory for multi-threaded program verification under sequential consistency, and we elaborate its theory solver, which realizes incremental consistency checking, minimal conflict clause generation, and specialized theory propagation to improve the efficiency of SMT solving. We conducted extensive experiments on credible benchmarks; the results show significant promotion of our approach.

　　Bio:   贺飞，博士，清华大学副教授。主要从事形式化方法、程序分析与验证、可满足性判定等方面的研究。主持开发了模型检测和软件验证的相关工具，并应用于航空、航天、高铁等国家重大安全领域。在包括POPL, CAV, PLDI, OOPSLA, ICSE, FSE, ASE, TSE, TOSEM, TDSC, TC等在内的国际重要会议和期刊上发表论文70余篇。现任《Theory of Computing Systems》、《Frontiers of Computer Science》编委，曾任CONCUR, FMCAD, APLAS, ICECCS, SETTA等重要国际学术会议的程序委员会委员。