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

这项为期两年的奖项为美法在验证硬件/软件计算机设计正确性方面的合作研究提供支持。该项目涉及犹他大学的Ganesh C.Gopalakrishnan和法国南希Henri Poincare大学的Dominique Mery的研究小组。美国的研究计划致力于开发为工业规模设计量身定做的正式方法。这些努力旨在制定正式的核查方法。法国关于应用于并发系统、时序逻辑和b-工具的形式化方法的研究计划，是对这家美国集团正在进行的研究的补充。该项目将增进对正式验证方法在计算机设计中应用的理解。

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.