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等重要國際學術會議的程序委員會委員。