Automated Formal Verification at the Hardware/Software Boundary

硬件/软件边界的自动形式验证

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

Computer chips, computer systems, and computer software are the most complex things ever designed by humans. For example, even the simple programs written by our students in their first computer science course have far more possible behaviors than there are photons in the universe! Not surprisingly, it's hard to get all the details right. In fact, companies now spend the most effort not on design, but on verification -- the task of determining if the system behaves correctly.

计算机芯片、计算机系统和计算机软件是人类有史以来设计的最复杂的东西。例如，即使是我们的学生在第一门计算机科学课程中编写的简单程序，其可能的行为也远远超过宇宙中的光子！毫不奇怪，很难把所有的细节都做对。事实上，公司现在花费最多的精力不是在设计上，而是在验证上--确定系统是否正确运行的任务。