Seminars

View all Seminars  |  Download ICal for this event

Formal Methods for Software Reliability and Synthesis

Series: CSA Colloquium

Speaker: Ashish Mishra

Date/Time: Feb 02 16:00:00

Location: CSA Seminar Hall (Room No. 254, First Floor)

Abstract:
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 _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) A 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_.

Speaker 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. Ashish is currently interested in using and extending the formal machinery of richer type systems for verifying and synthesizing programs. 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 the workforce) and others involved in Media Monitoring and Research.

Host Faculty: K. V. Raghavan