CAREER: Lightweight, Blame-aware Contract Checking

Northwestern University, Evanston IL

Investigators

Abstract

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5). As computers become more powerful, the limiting factor for building software systems is shifting away from the underlying computer's performance limitations to the software's inherent complexity. One way to cope with this complexity is to use software contracts to separate a large system into smaller chunks, thereby enabling programmers to focus their energy on just one small part of the system at a time. A key feature of this separation is the ability to assign blame; that is, when the software system fails, a contract checker can use the contracts to identify a single sub-system as faulty, automatically narrowing the search for the underlying cause of the failure to that one subsystem or possibly its contract; of course, fixing a bug in a contract may yet expose latent bugs in other subsystems but in each case the contract system will help the programmer identify the failure. Even better, software contracts are typically written in a language that is very close to the programming language, meaning that programmers only have to invest a little bit of their time and resources in order to start seeing the benefits of contracts. This work promises to improve the state of the art in contract checking. Specifically, the PI will study the interaction between statically and dynamically verified portions of systems, in a manner similar to hybrid and gradual types. Building on this integration, the PI will also study how to integrate theorem provers into software systems in a way that the theorem prover's scope can be limited to just the most mission-critical parts of the system. The PI will also study how to add contracts to more sophisticated modularity mechanisms like traits and the ML module system, and explore how contracts can help generalize existing techniques for automatic test case and test oracle generation to support higher-order functions and unknown classes. All the while, the PI will ensure that these new techniques are practically viable by using them in a 500,000 line software system that the he maintains, as well as conducting detailed studies of how contracts are used in other settings, including JML and Eiffel.