Practical formal methods for software analysis and development

Formal methods techniques for improving software correctness and reliability fall into two categories, namely, program analysis and program synthesis. Program analysis techniques automatically find defects (or prove the absence thereof) in existing software. In a dual way, program synthesis techniques generate correct-by-construction code from high-level specifications. In this thesis, we propose an array of formal method techniques that further improve the state-of-the-art of program analysis techniques, while also applying program synthesis techniques in previously unexplored domains.

Broadly speaking, the long history of program analysis can be summarized as the battle between precision and scalability. As a first step in this thesis, we propose a technique called program trimming that helps arbitrary safety-checking tools to achieve a better balance between precision and scalability. In a nutshell, program trimming semantically simplifies the program by eliminating provably correct execution paths. Because the number of execution paths is a typical scalability bottleneck for some techniques (e.g., symbolic execution) and a source of imprecision for others (e.g., abstract interpretation), program trimming can be used to improve both precision and scalability of program analysis tools. We have implemented our technique in a tool called Trimmer and showed that Trimmer significantly improves the behavior of two different program analyzers over a set of challenging verification benchmarks.

Program synthesis, on the other hand, has only recently started to appear in more practical aspects of software development. Formal method techniques in this area aim to ease programming for several domains while targeting a broad range of programmers, from novices to experts. In this thesis, we propose a novel program synthesis technique, implemented in a tool called Expresso, that aids experts in writing correct and efficient concurrent programs. Specifically, Expresso allows programmers to implement concurrent programs using the implicit signaling paradigm, where the programmer specifies the condition under which a thread should block but she does not need to worry about explicitly signaling other threads when this condition becomes true. Given such an implicit signaling program, Expresso generates an efficient and correct-by-construction program that does not contain deadlocks caused by improper signaling. Our evaluation shows that Expresso is able to synthesize efficient implementations of real-world monitors with performance comparable to the one written by programming experts.

Finally, we observe that certain monitors require their clients to use their API in a manner that conforms to a context-free specification. Statically verifying that a client conforms to a context-free API protocol cannot be handled by any prior technique. To rectify this and ensure that client applications properly use such protocols, we propose CFPChecker, a tool that verifies the correct usage of context-free API protocols. Given a program, P, and an API protocol expressed as a parameterized context-free grammar, GS, CFPChecker either proves that P conforms to GS or provides a genuine program trace that demonstrates an API misuse. We have evaluated our proposed technique on a wide variety of popular context-free API protocols and several clients drawn from popular open-source applications. Our experiments show that CFPChecker is effective in both verifying the correct usage and finding counterexamples of context-free API protocols.