[FM-India]IARCS Verification Seminar Series -- Talk by Ashish Mishra on April 07 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Ashish Mishra, a faculty member in the Department of Computer Science and Engineering at IIT Hyderabad. The talk is scheduled on Tuesday, April 07, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NG8ydXZuaW9lNGwxcWpwcDgxamZzaXZtYWwgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Organizers, IARCS Verification Seminar Series ============================================================= Title: Coverage Types: Underapproximate Refinement Types for Generator Coverage Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: Property-based testing (PBT) has become a widely used technique for validating semantic properties of programs by automatically generating test inputs that satisfy user-specified preconditions. In practice, however, the effectiveness of PBT depends critically on the quality of input generators. When preconditions describe rich structural constraints, purely random generators rarely produce many valid inputs, forcing developers to write specialized generators by hand. Unfortunately, such generators are often incomplete, i.e., they may fail to produce many valid inputs, limiting the behaviors explored during testing. However, it is not readily apparent how to validate whether a particular generator provides sufficient coverage against a given precondition. Typically, developers must rely on manual inspection and post-hoc analysis. In this talk, I will present a refinement type-based framework for reasoning about the coverage of test input generators. Our key idea is coverage types, an interpretation of refinement types that captures must-style guarantees about the values a program will produce, rather than the traditional may-style approximation of possible outputs. Conceptually, coverage types bring ideas from Incorrectness logic and underapproximate reasoning into the type system. The types associated with expressions now capture the set of values guaranteed to be produced by an expression, rather than the typical formulation that uses types to represent the set of values an expression may produce. This automated, underapproximate reasoning mechanism allows us to formally verify coverage properties of generators in a higher-order functional language with inductive data types. Building on this foundation, I will also describe a synthesis-based program repair technique that automatically patches incomplete generators by enumerating candidate repairs guided by coverage types. Together, these ideas enable both verification and automated repair of test generators, providing stronger guarantees about the effectiveness of property-based testing and illustrating how incorrectness-style, underapproximate reasoning can be integrated with modern type systems to support practical testing workflows. Bio: Ashish Mishra obtained his PhD from IISc Bangalore. He was subsequently a post-doctoral researcher at Northeastern University and Purdue University, before joining IIT Hyderabad as an Assistant Professor in 2024. Ashish's research interests are broadly in Program Verification and Synthesis, Functional Programming and Type Systems.