信息讨论班——Compositional Verification of Programs
主 题: 信息讨论班——Compositional Verification of Programs
报告人: SUN Jun (新加坡科技设计大学)
时 间: 2016-12-06 14:00 - 15:00
地 点: 理科一号楼 1303
The answer to the question - how do we verify real programs - is perhaps already answered by how we develop programs. We know that already - abstraction, composition and hierarchy. In developing a big program, each time we focus on a component of the system and use it abstractly afterwards. In this work, we explore the idea of compositional verification which aims to do the same for verifying programs. The idea is of compositional verification is to focus on verifying one component at a time, and establish system-level property based on properties on the verified components. The challenges are twofold. Firstly, a component doesn't function on its own and thus how do we obtain minimum knowledge of the rest of the system so that the component can be verified? Secondly, how do we decide what the components are?
