Machine-assisted theorem proving: Proof techniques and applications

提出的研究的主要目标是推进程序、编程语言和策略属性的形式化证明技术。对于单个程序，证明它们满足某些属性有助于非常高水平地保证它们将按照预期的方式运行。对于编程语言的属性，众所周知，那些被正式证明是可靠的语言可以更好地为构建可靠和安全的软件系统提供坚实的基础。政策发挥日益重要作用的例子包括确保处理健康或其他个人数据的软件尊重隐私要求，以及确保用于企业管理的软件尊重政府的财务和安全法规。

The principle objective of the proposed research is to advance techniques in formal proof of properties of programs, programming languages, and policies. For individual programs, proving that they meet certain properties contributes to a very high level of assurance that they will behave as expected. For properties of programming languages, it is well-known that those that are formally proven to be sound can better provide a solid basis for building software systems that are reliable and secure. Examples where policies play an increasingly important role include assuring that software that processes health or other personal data respects privacy requirements, and assuring that software that is used in the administration of businesses respects government financial and security regulations.