U.S.-France Cooperative Research: Formal Methods for Secure and Reliable Hardware/Software Design

美法合作研究：安全可靠的硬件/软件设计的形式化方法

• 批准号: 9726717
• 负责人: Ganesh Gopalakrishnan
• 金额: $ 0.98万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-04-01 至 2001-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9726717&HistoricalAwards=false
• 关键词: U.S.; France; Cooperative; Research; Formal

This two-year award provides support for US-France cooperative research on verifying the correctness of hardware/software computer designs. The project involves the research groups of Ganesh C. Gopalakrishnan at the University of Utah and Dominique Mery of the University Henri Poincare in Nancy, France. The US research program addresses the development of formal methods tailored for industrial-scale designs. These efforts are aimed at the development of formal verification methods. The French research program on formal methods applied to concurrent systems, temporal logic and b-tools complements the ongoing research of the US group. The project will advance understanding of the application of formal verification methods to computer design.

这个为期两年的奖项为美法合作研究提供支持， 计算机硬件/软件设计的正确性。 该项目涉及研究 Ganesh C.犹他州大学的Gopalakrishnan和明尼苏达州的Dominique Mery 法国南希的亨利·庞加莱大学。 美国的研究计划解决了 开发适合工业规模设计的正式方法。 这些努力 目的是发展正式的核查方法。 法国研究计划 关于并发系统的形式化方法，时态逻辑和b工具补充 该美国小组正在进行的研究。 该项目将促进对 形式验证方法在计算机设计中的应用。