We present a counterexample-driven algorithm to infer provably sufficient representation invariants that certify correctness of data-structure implementations. Our implementation, Hanoi, can automatically infer representation invariants for several common recursive data structures, such as sets, lists, trees, etc.
We define overfitting in the context of CEGIS-based SyGuS, and show that there exists a tradeoff between expressiveness and performance. We present two mitigation strategies: (1) a black-box approach that any existing tool can use, and (2) a white-box technique called hybrid enumeration.
We propose a static analysis for slicing functional programs, which precisely captures structure-transmitted dependencies and provides a weak form of context sensitivity — weakened to guarantee decidability. We also show an incremental version this technique that is efficient in practice.
We present a technique, called the precondition inference engine (PIE), which uses on-demand feature learning to automatically infer a precondition that would satisfy a given postcondition. We use PIE to also construct a novel automatic verification system called LoopInvGen.
We present a technique, called FlashProfile, to generate hierarchical data profiles. Existing tools, including commercial ones, generate a single flat profile, and are often overly general or incomplete. Furthermore, we show that data profiles can improve accuracy and efficiency of PBE techniques.
We present regression-based models for predicting ChromeOS user experience metrics from hardware specifications of Chromebook laptops.
We present a collection of automated analyzers that help AWS customers verify that their IoT Event detector models are free of common defects.
We present a new approach to synthesizing provably sufficient loop invariants by leveraging integer linear programming (ILP).