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

该项目支持德克萨斯农工大学（TAMU）的研究人员和法国的同事之间的一个独特而重要的合作计划，以改进最广泛使用的编程语言之一c++。世界经济的安全关键部门，如空中交通管制，依赖于用c++编写的系统软件。尽管有国际标准，有非常大的用户社区，在全球经济中也有相应的分量，但是没有可靠的、可扩展的方法来正确地、机械地将c++程序转换为可执行的机器码。该奖项将资助TAMU的Gabriel Dos Reis博士和他的三名学生，与法国罗昆古国际信息技术研究所的Xavier 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.