Automatically Synthesizing Structured Input Generators

Overview

The goal of this project is to build PL/formal methods-based technology, in combination with GenAI, that can automate the synthesis of test input generators. Such generators are useful property-based testing, model-based testing, differential testing, fuzz testing, and other automated testing setups. Generators for complex inputs formats, such as those used for testing compilers, are quite labor intensive to write by hand, and they are easy to get wrong. Our goal is to bring proof-based technology in the Lean programming language together with the power of GenAI to produce efficient, effective, and proved correct generators.

Project Status

Under development.