| Title | : | Automated Type-Based Verification of Test Input Generators or A Type System for Incorrectness |
| Speaker | : | Prof. Suresh Jagannathan (Professor, Computer Science @ Purdue University) |
| Details | : | Tue, 19 Mar, 2024 4:00 PM @ SSB-334 |
| Abstract: | : | Program verifiers validate the correctness of a safety specification with respect to the set of possible behaviors a program may exhibit. Typically, this set represents an over-approximation of possible execution states. Dually, we might reason about a program's behavior with respect to a coverage property that uses under-approximate reasoning to characterize a set of feasible executions, i.e., executions a program must exhibit. Coverage is a particularly useful notion for formalizing the behavior of applications like thread schedulers, symbolic execution tools, or test input generators, all of which are designed to systematically explore a large state space. In this talk, we explore how we might use coverage to verify the correctness of property-based testing (PBT) frameworks. Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by PBT generators can be complex data structures, constrained to satisfy properties the developer believes is most relevant to testing the function of interest. Developers expect generators to be capable of producing all acceptable elements that satisfy the function's input type and generator-provided constraints. However, determining if a generator provides sufficient coverage typically requires manual inspection and post-mortem analysis of test runs, mechanisms that are error-prone and difficult to scale as generators become more complex. To address this shortcoming, we present a new automated refinement type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds ``must-style'' underapproximate reasoning principles as a fundamental part of the type system. Our formulation can be thought as an initial attempt to provide a type-theoretic characterization of recently proposed Incorrectness Logics to reason about a program's completeness properties. We also discuss promising experimental results of a coverage type system implemented for OCaml. This is joint work with Zhe Zhou, Ashish Mishra, and Benjamin Delaware. |
