CAREER: Modular Verification of Software

University Of California-Los Angeles, Los Angeles CA

Investigators

Abstract

ABSTRACT 0546170 Rupak Majumdar University of California - Los Angeles, Modular Verification of Software Majumdar Intellectual Merits. Writing correct software is hard. Our techniques to ensure software reliability lag far behind our requirements for more and more complex systems. Unlike for lowlevel correctness requirements (such as correct syntax, or correct use of types), application level properties are currently not specifiable or automatically checkable. Testing remains the dominant methodology to ensure software quality with regard to application level properties, however, it is not exhaustive, and nasty bugs are often exposed post-deployment. Thus, the availability of analyses that can automatically check higher-level properties of large software systems soundly and precisely will mark a major advance in our ability to develop more reliable software. This project leverages recent advances in software verification and explores new ideas to significantly extend the capabilities of modern verification tools to handle larger programs and more complex properties. We contend that the leap to scalably verifying end-to-end properties of software will be enabled by novel techniques in modular software verification, over and above existing techniques like model checking, predicate abstraction, and abstraction refinement. While the basic principles of modularity in system verification have been known for decades, they have not been widely adopted in program analysis tools because there is no push-button way to apply them in full generality. We focus on the technical challenges in automating modular verification by studying the following widely occurring verification patterns. Tighter integration of type information in model checking through predicated types. Automatically synthesizing temporal interfaces that specify behavioral requirements. Integration of abstract data types into symbolic reasoning. Automatic parameterized verification through design decomposition. Our research will immediately benefit any large software system where robustness and reliability are pressing concerns; we shall validate our research by verifying end-to-end properties of enterprise applications and high performance servers from which we derived the verification patterns and which are beyond the scope of current tools.