Our modern society increasingly depends on the reliability, safety, and security of computer software. However, the compilers and other tools that analyze and translate the software into executable form can create a critical bottleneck: if a compiler has an error, then any software compiled by it may in turn be compromised.
This project addresses this fundamental problem by developing effective, efficient, and correct language and tool implementation technology. Central to the project is that program analyses and transformations, the heart of optimizing compilers and software analysis tools, are written in a specialized language, named Rhodium. By focusing on this domain, it becomes feasible to build a fully-automatic correctness checker that ensures that Rhodium analyses and transformations are guaranteed to preserve the behavior of any program they process.
Previous work developed a proof-of-concept Rhodium system, and demonstrated it on a range of intraprocedural optimizations. This project is developing new techniques that will allow the Rhodium system to scale to richer and more realistic settings, including the ability to optimize full-featured object-oriented and functional languages, perform scalable interprocedural analyses, execute with high efficiency, and cover the full range of tasks in the "middle-end" of optimizing compilers and software checking tools.
