projects

Some Representative Research Projects in the group.

Below are some of the research projects pursued in our group; besides these, there are several research ideas and directions under exploration:

Fundamentals: Verification and Synthesis.

This umbrella project aims to make fundamental contributions towards using Refinement Types for verification and synthesis. We are developing novel type systems and domain-specific languages aimed at:

• Verify under-approximate properties of programs using novel Coverage Types.

• Verifying properties of higher-order parser combinators using Morpheus.

• Scalable component-based program synthesis over refinement-typed libraries using Novel tree automata representation Hegel.

• Synthesizing coverage complete programs using Coverage Types Cobb.

Neurosymbolic Program and Specification Synthesis.

Neurosymbolic Programming is a promising new area at the intersection of program synthesis and machine learning. The main goal of this project is to develop novel NeuroSymbolic techniques and tools to address the limitations of both Neural and Symbolic approaches. We are working towards expanding the state-of-the-art in program synthesis, allowing synthesis of efficient, robust, and verified programs for challenging low-level, safety-critical programming tasks.

Synthesis in Novel Domains.

This parent project aims to solve challenging and error-prone programming tasks in various domains using program synthesis.

• DUNE: Multi-Modal, NeuroSymbolic Synthesis for Automatic Data Transformation:

• TANTRA: Automated generation of correct low-level network configuration files from high-level network properties.

Trustworthy Parallelism at Scale.

Under this project, we aim to develop (semi)automated and scalable reasoning methods and tools—with predictable performance guarantees—to detect and analyze undesired behaviors in AI workloads executed across CPUs, GPUs, and emerging accelerators.