Automated Software Verification: Foundations and Applications

自动化软件验证：基础和应用

• 批准号: RGPIN-2017-03998
• 负责人: Gurfinkel, Arie
• 金额: $ 2.48万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2017
• 资助国家: 加拿大
• 起止时间: 2017-01-01 至 2018-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=634596
• 关键词: Automated; Software; Verification; Foundations; Applications

Modern software systems are incredibly complex engineered artifacts. They rely on intricate algorithms, developed by large, often distributed, teams, and are build out of many interconnected components. Software systems are extremely difficult to get right, to verify, and to certify. Software bugs are common even in such safety-critical industries as medical devices, automotive, and avionics. Yet, our society is increasingly becoming dependent on reliable operation of such systems. The border between safety- and non-safety-critical system is being eroded.

现代软件系统是极其复杂的工程制品。它们依赖于复杂的算法，这些算法由大型且通常是分布式的团队开发，并且由许多互连的组件构建而成。软件系统的正确性、验证和认证极其困难。即使在医疗设备、汽车和航空电子设备等安全关键行业，软件错误也很常见。然而，我们的社会越来越依赖于此类系统的可靠运行。安全关键系统和非安全关键系统之间的界限正在被侵蚀。