Planning Visits: Building a Coalition for Provably Correct C++ Program Translation

该项目支持德克萨斯农工大学(TAMU)的研究人员和法国同事之间独特而重要的合作计划，以改进C++这一使用最广泛的编程语言之一。世界经济中对安全至关重要的部门，如空中交通管制，依赖于用C++编写的系统软件。尽管存在国际标准，以及非常大的用户社区和在全球经济中的相应权重，但没有可靠和可扩展的方法来正确和机械地将C++程序转换为可执行的机器代码。该奖项将资助TAMU的Gabriel Dos Reis博士和他的三名学生花时间与法国INRIA Rocquencourt的Xille Leroy博士合作，发展强大的研究伙伴关系，以提高C++编译器的可靠性。这种合作是独一无二的，因为它建立在研究人员各自的优势之上：美国团队拥有C++编程语言标准和C++编译器方面的专业知识，而法国团队则为嵌入式系统的实际编译器提供正式方法方面的专业知识。法国团队为C编程语言的实际子集开发的正式方法将被美国团队用于追求C++对象模型的机械化，特别是对于新的语言功能。

This project supports the planning of a unique and important collaboration between researchers at Texas A&M University (TAMU) and colleagues in France to improve C++, one of the most widely used programming languages. Safety-critical sectors of the world economy, such as air-traffic controls, rely on systems software written in C++. Despite the existence of international standards, and a very large users' community and corresponding weight on the global economy, there is no reliable and scalable way to correctly and mechanically translate C++ programs into executable machine codes. This award will fund Dr. Gabriel Dos Reis from TAMU and three of his students to spend time working with Dr. Xavier Leroy at INRIA Rocquencourt in France to develop a strong research partnership to improve the reliability of C++ compilers. This collaboration is unique because it builds on the respective strengths of the researchers: while the U.S. team has expertise with the C++ programming language standards and C++ compilers, the French team provides expertise in formal methods for realistic compilers for embedded systems. The formal methods developed by the French team for a realistic subset of the C programming language will be used by the U.S. team in its pursuit of mechanization of the C++ object model, especially for new language features.