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.
