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

Texas A&M Engineering Experiment Station, College Station TX

Investigators

Abstract

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.