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

计划访问：建立可证明正确的 C 程序翻译联盟

• 批准号: 1043084
• 负责人: Gabriel Dos Reis
• 金额: $ 2万
• 依托单位: Texas A&M Engineering Experiment Station
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-12-01 至 2012-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1043084&HistoricalAwards=false
• 关键词: Planning; Visits; Building; Coalition; Provably

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.

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