报告标题：Toward Efficient Verification of the Finite Variant Property
报告时间：4月21日14：00-15：30
报告地点：理科大楼B1002
报告摘要：
Modern security protocols are used everywhere, from online banking and messaging apps to digital authentication systems. To ensure that these protocols are secure, researchers often rely on formal verification tools, such as ProVerif and Tamarin.
A central challenge in this area is unification modulo an equational theory. In practice, most automated verifiers focus on equational theories that satisfy the Finite Variant Property (FVP), for which solving unification is decidable. However, such tools often require users either to prove the FVP manually or to provide a special representation of the theory, which limits their usability in practice. Recent work has made automatic verification of the FVP possible, but the current method still faces significant efficiency challenges.
In this talk, I will present our recent work on improving the efficiency of FVP verification by flattening. I will explain the motivation for this problem, the practical challenges involved, and the main ideas behind our approach.
报告人简介：
Jiachen Qian is a second year DPhil (PhD) student in Computer Science at the University of Oxford, supervised by Vincent Cheval. His research focuses on formal methods and automated reasoning, especially equational reasoning and symbolic verification of security protocols. Before starting his DPhil, he studied Mathematics at the University of Sheffield and later completed an MSc in Mathematics and Foundations of Computer Science at Oxford.