Chennai Mathematical Institute

Seminars




Computer Science Seminar
Date: Thursday, 03 August 2023
Time: 09:00 - 10.00 PM
Venue: Virtual Mode
Formal Methods for Software Reliability and Synthesis

Ashish Mishra
Purdue University.
03-08-2023


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, thereby achieving the long-dreamt reliability goals while making programming as a discipline more democratic and accessible to the masses? My current and future research is a step toward answering this question in the affirmative.
In this talk, I will begin by highlighting some of these overarching research interests and directions. I will present two of my recent works highlighting the effective use of Refinement types, DSLs, and SMT-based techniques for the verification and synthesis of effectful programs.
(i) The first one is a new 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-Typed DSL for developing safe, verified, combinator-based parsers. It presents a deeply-embedded DSL for OCaml called Morpheus that we use to express and verify parsers and the combinators that compose them. It provides a novel automated verification pathway for Parser Combinator programs.
In the final remarks, I will discuss some of my other works, ongoing works, and future research directions. Particularly, I will discuss three potential paths: (i) A few fundamental challenges/opportunities in program verification and synthesis and potential solutions to some of these; (ii) Applying program synthesis to novel domains like Robotics; (iii) Combining Neural and Symbolic program synthesis approaches, aka Neurosymbolic program synthesis.
Speaker Bio: Ashish Mishra completed his MS (Engineering) and PhD Computer Science at IISc in 2018. He has since been a postdoctoral researcher at Northeastern University and Purdue University. His research interests are in Programming Languages, Formal Verification, Program Analysis, Program Synthesis, Type Systems, Neural + Symbolic Synthesis.