Mechanised foundations of proof calculi

证明演算的机械化基础

• 批准号: DP120101244
• 负责人: Prof Rajeev Gore
• 金额: $ 25.22万
• 依托单位: The Australian National University
• 依托单位国家: 澳大利亚
• 项目类别: Discovery Projects
• 财政年份: 2012
• 资助国家: 澳大利亚
• 起止时间: 2012-01-30 至 2016-12-31
• 项目状态: 已结题
• 来源: https://dataportal.arc.gov.au/RGS/Web/Grants/DP120101244
• 关键词: Mechanised; foundations; proof; calculi

Commercial program verification tools based upon special-purpose logic-based proof calculi can now guarantee that large programs are free of specific bugs. But who verifies the proof-calculi? Our research will lead to tools to automatically verify proof-calculi and will eventually help to avoid costly post-construction debugging.

基于专用逻辑证明演算的商业程序验证工具现在可以保证大型程序没有特定的错误。但谁来验证演算的证明呢？我们的研究将导致自动验证证明演算的工具，并最终有助于避免昂贵的施工后调试。