Building reliable software systems remains a challenging problem. The main difficulty is that such systems are built by integrating smaller components written by developers working in isolation. Each component functions correctly only under some specific conditions that remain unarticulated in the development process, thereby complicating the task of checking the compatibility of the different parts.
This research proposes to develop Assert-Generated Interfaces, a toolkit to increase the reliability of software by ensuring that large systems are built from compatible components. Individual component builders then locally specify properties critical to the correct working of the components using assert statements embedded within the implementation.
These assertions are automatically analyzed to obtain interfaces that describe how the component may be safely used. Automatic generation ensures the interface evolves with the implementation. Assert Generated Interfaces decompose the task of system-level correctness checking into manageable component-level checks, and when static checking is impossible, the interfaces can be used to build wrappers that dynamically shield components by blocking unsafe uses.
This project led to the several distinct and important outcomes, allrelated to the general idea of modular and compositional analysis ofsoftware system via inferring appropriate interfaces. Intellectual Merit 1. Liquid Types The most significant outcome is the development of the technique ofliquid types, which shows how advances in SMT solvers can be used toenrich vanilla type signatures with very precise information aboutthe behavior of components. Additionally, through types, we areable to address the problem of analyzing unbounded data structures that has been a long standing problem in software verification.Going forward, we believe that this combination of powerful logic machinery(SMT) with the most widely used formal method for ensuring reliability(types) will have a significant impact on ensuring the compatibilityand composability of software components from different sources. 2. RELAY Race Detector The second most significant outcome is the design, implementation andevaluation of scalable tools for concurrency analysis based on the notionof "Relative LockSets". The resulting RELAY race detector was the firstto scale to million line code bases, and was the basis of a generictechnique for data flow analysis of concurrent programs. Broader Impact The liquid types work was published in a series of papers at the very topvenues in the field. While the work was done originally in the context ofOCAML and C, it has now been extended by others to other languages,different kinds of properties -- from compiler optimizations to securityand deterministic parallelism. The lead student (Patrick Rondon's) PhD dissertation received the SIGPLAN Distinguished Dissertation Award. From the citation: "Patrick Rondon’s dissertation makes several significant contributions tothe field of automatic program verification. It takes a type system -- ahighly scalable yet not quite precise method of dealing with programs --and refines it using Satisfiability Modulo Theory (SMT) techniques tocompensate for the precision loss. There are implementations for both OCamland C. The achieved degree of effectiveness and automation is astonishing:programs that are beyond the existing verification tools can be handledfully automatically within seconds. It demonstrates that formalverification can yield significant reliability guarantees for mainstreamsoftware engineering, at a reasonable cost." The project supported the PhD theses of three students: 1. Patrick Rondon 2. Ming Kawaguchi 3. Jan Voung The source code for RELAY, DSOLVE (liquid types for Ocaml) and CSOLVE(liquid types for C) have been publicly released and used already byseveral other groups that have started working on related areas.
