Machine-assisted theorem proving: Proof techniques and applications

机器辅助定理证明：证明技术和应用

• 批准号: 227798-2009
• 负责人: Felty, Amy
• 金额: $ 2.55万
• 依托单位: University of Ottawa
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2013
• 资助国家: 加拿大
• 起止时间: 2013-01-01 至 2014-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=524110
• 关键词: Machine; assisted; theorem; proving; Proof

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.

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