Building reliable software has been a classical goal in Computer Science.
The most basic premise of my research is derived from this goal. Can we make programs safe and reliable using formal techniques while making programming as a discipline more democratic and accessible to the masses?
In this talk, I will begin by highlighting some of these overarching research interests and directions.
I will primarily present two of my recent works highlighting the effective use of Refinement types and SMT-based techniques for the _verification_ and _synthesis_ of programs.
(i) The first is a specification-guided _synthesis_ procedure that uses Hoare-style pre- and post-conditions to express fine-grained effects of potential library component candidates to drive a bi-directional synthesis search strategy. It integrates a conflict-driven learning procedure into the synthesis algorithm that provides a semantic characterization of previously encountered unsuccessful search paths used to prune possible candidates' space as synthesis proceeds.
(ii) The second work is a new _Refinement-Type_ system called _Coverage Type_ which adapts the recent work in Incorrectness Logic to the specification and automated verification of test input generators used in modern property-based testing systems. Specifications are expressed in the language of refinement types, augmented with coverage types, types that reflect underapproximate constraints on program behavior.
I will conclude with some of my completed and ongoing works and future research directions.
Particularly, I will discuss three potential paths I am taking:
(i) Our new deductive CBS using _Semantic Similarity Reduction_ based on a novel definition of a _Qualified Tree Automata_.
(ii) Utilizing _underapproximate_ reasoning for deductive synthesis.
(iii) Applying program synthesis to _novel domains_ like Robotics and the need for combining Neural and Symbolic program synthesis approaches, aka _Neurosymbolic program synthesis_.
Short Bio:
Ashish Mishra is a Postdoctoral Researcher at Purdue University, where he works with Professor Suresh Jagannathan in the areas of Programming Languages, Program Verification, and Program Synthesis.
Ashish obtained his Ph.D. from the Indian Institute of Science, where he worked under the supervision of Professor Y. N. Srikant.
In addition to his work in Computer Science, Ashish is also interested in applying technology to public policies and solving social problems. He is currently involved with several Indian NGOs such as PARI (People's Archive for Rural India), Mosali (a startup trying to bring women into workforce), and others that are involved in Media Monitoring and Research.
