PurForM

Ongoing Projects
Discover[i]
Automate aspects of programming distributed applications by developing new foundations, algorithms and tools for synthesis and verification of distributed applications built using verified components and parameterized by the number of processes.
Publications preprint
Robust Example-based Synthesis
Develop a principled approach based on formal methods, relational reasoning, and computational learning theory for the design and analysis of example-based program synthesizers. The key insight is to cast the problem of reliability of these systems as one of robustness: is the change in the synthesized program acceptable, or, at least predictable, in the presence of small changes to the set of examples?
Publications preprint
Personalized Education
Build effective tools for automated reasoning about programming assignments at scale based on program analysis, program repair, program synthesis and machine learning.
Publications PLDI19, CAV16, SAS14
Tools Qlose
Safe and Robust AI
Enable construction of provably safe and robust machine learning applications through effective integration of symbolic reasoning, probabilistic inference and continuous optimization.
Completed Projects
Synchronization Synthesis
Developed advanced trace-based techniques for synchronization synthesis and applied them to device driver programming. Our work resulted in new contributions in language theoretic-verification, trace generalization and synchronization inference.
Publications FMSD16, CAV15, POPL15
Tools TARA, LISS, LIMI
Robust Transducers
Formalized robustness of finite-state I/O systems as Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input - and developed automata-theoretic decision procedures for checking K-robustness of discrete transducers, networks of discrete transducers, timed transducers, and asynchronous sequential circuits.
Publications VMCAI16, FSTTCS14, ATVA13, VMCAI13