报告题目：Static model checking of concurrent systems

报告人：Bill Roscoe 教授

主持人：何积丰

报告时间：6月13日（周二）14:00-15:30

报告地点：中北校区数学馆201室

报告摘要：

We are constantly seeking ways of overcoming the state explosion problem in model checking.  SAT checking has not so far worked well for the exact checking of properties of concurrent systems.  It is thought that this is because reachability in such systems is PSpace-hard, beyond the comfort level of SAT checking, and indeed even our attempts at bounded model checking here have worked poorly.  We have, however, found a new approximate approach to this problem.  This is based on building local information about what combinations of states of parallel components are mutually reachable, and then giving a SAT checker the job of discovering if there is a global assignment of states which satisfies such constraints and which fails a desired specification.  For example by seeking an assignment where every component is blocked we can check (conservatively) for deadlock freedom.

Such checks can be tightened up by adding in invariants we know to be true in the network.  For example, with a separate SAT check, we can look for a token invariant (or perhaps more than one) in the network without even knowing there is one.

报告人简介：

Prof. Bill Roscoe is a Scottish computer scientist. He was Head of the Department of Computer Science, University of Oxford from 2003-2014, and is a professor of Computer Science. He is also a fellow of University of College, Oxford.

Professor Roscoe works in the area of concurrency theory, in particular the semantic underpinning of Communicating Sequential Processes (CSP) and the associated Occam programming language with Sir Tony Hoare. He co-founded Formal Systems (Europe) Limited and worked on the algorithms for the Failures-Divergence Refinement (FDR) tool.