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.