What-Comes-Next (WCN) puzzles challenge us to identify the next figure that "logically follows" a provided sequence of figures. WCN puzzles are a favorite of interviewers and examiners---there is hardly any aptitude test that misses WCN puzzles. In this work, we propose to automatically synthesize WCN puzzles. The key insight to our methodology is that generation of WCN problems can be posed as a program synthesis problem. We design a small yet expressive language, PuzzlerLang, to capture solutions to WCN puzzles. PuzzlerLang is expressive enough to explain almost all human generated WCN puzzles that we collected, and yet, small enough to allow synthesis in a reasonable time. To ensure that the generated puzzles are appealing to humans, we infer a machine learning model to approximate the appeal factor of given WCN puzzle to humans. We use this model within our puzzle synthesizer as an optimization function to generate highly appealing and correct-by-construction WCN puzzles. We implemented our ideas in a tool, PuzzleGen; we found that PuzzleGen is fast, clocking an average time of about 3.4s per puzzle. Further, statistical tests over the responses from a user-study supported that the PuzzleGen generated puzzles were indistinguishable from puzzles created by humans.

Program analysis, verification and testing are important topics in programming languages and software engineering. They aim to produce engineers who are not only capable of empirically evaluating but, also formally reasoning on the correctness of software systems. We propose a specialized framework, Chiron, designed to teach graduate-level courses on these topics. Chiron has a small code base for easy understanding, uses a unified intermediate representation across all its analysis modules, maintains a modular architecture for plugging in new algorithms and uses a “fun” programming language to provide a gamified experience. Currently, it packages a dataflow analysis engine for driving compiler optimizations, an abstract interpretation engine for verification, a symbolic execution engine, a fuzzer and an evolutionary test generator for program testing, and a spectrum based statistical bug localization module. Within Chiron, program analysis tasks are posed in an unconventional setting (as adventures of a turtle) to provide a gamified experience; the accompanying animations (showing the movements of the turtle) allow the student to understand the underlying concepts better, and the detailed logs allow the teaching assistants in their grading activities. Chiron has been used in two offerings of a graduate level course on program analysis, verification and testing. In response to our survey questionnaire, all the students unanimously held the opinion that Chiron was extremely helpful in aiding their learning, and recommended its use in similar courses.

Real-life programs contain multiple operations whose semantics are unavailable to verification engines, like third-party library calls, inline assembly and SIMD instructions, special compiler-provided primitives, and queries to uninterpretable machine learning models. Even with the exceptional success story of program verification, synthesis of inductive invariants for such "open" programs has remained a challenge. Currently, this problem is handled by manually "closing" the program---by providing hand-written stubs that attempt to capture the behavior of the unmodelled operations; writing stubs is not only difficult and tedious, but the stubs are often incorrect---raising serious questions on the whole endeavor. In this work, we propose Almost Correct Invariants as an automated strategy for synthesizing inductive invariants for such "open" programs. We adopt an active learning strategy where a data-driven learner proposes candidate invariants. In deviation from prior work that attempt to verify invariants, we attempt to falsify the invariants: we reduce the falsification problem to a set of reachability checks on non-deterministic programs; we ride on the success of modern fuzzers to answer these reachability queries. Our tool, Achar, automatically synthesizes inductive invariants that are sufficient to prove the correctness of the target programs. We compare Achar with a state-of-the-art invariant synthesis tool that employs theorem proving on formulae built over the program source. Though Achar is without strong soundness guarantees, our experiments show that even when we provide almost no access to the program source, Achar outperforms the state-of-the-art invariant generator that has complete access to the source. We also evaluate Achar on programs that current invariant synthesis engines cannot handle---programs that invoke external library calls, inline assembly, and queries to convolution neural networks; Achar successfully infers the necessary inductive invariants within a reasonable time.

We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and can prove probabilistic properties that universally quantify over all possible inputs. Our technique augments standard symbolic execution with a new class of probabilistic symbolic variables , which represent the results of random draws, and computes symbolic expressions representing the probability of taking individual paths. We implement our method on top of the KLEE symbolic execution engine alongside multiple optimizations and use it to prove properties about probabilities and expected values for a range of challenging case studies written in C++, including Freivalds’ algorithm, randomized quicksort, and a randomized property-testing algorithm for monotonicity. We evaluate our method against Psi, an exact probabilistic symbolic inference engine, and Storm, a probabilistic model checker, and show that our method significantly outperforms both tools.