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.