This project investigates techniques and tools for assuring software quality: finding and removing defects in software systems, as well as improving current methodology for designing high-quality software systems at the outset. The project consists of both experimental and theoretical components.
The experimental effort is focused on designing and building tools to improve the quality of Open Source software. Open Source is attractive as a research vehicle in software quality because of the critical role it plays in the nation's economy and precisely because it has the unique feature that it is a real-world system that is completely open and available for study. Because of the Open Source tradition of incorporating useful new techniques and tools into the Open Source environment, there is also an opportunity for direct and widespread impact.
The foundational work in this project combines expertise in the three branches of the discipline of the analysis of software: formal verification and theorem proving, model checking, and large-scale software analysis. These three areas have developed rapidly in recent years, seeing both significant theoretical and practical advances. A central thesis of this project is that significant further advances are possible by bringing together these areas to work on a common set of problems.
You can go here to read about our projects, or here to meet the group members.
Page maintained by Joel Galenson.