Professor Parthasarathy applies formal methods to the development of trustworthy software. The Java Interface Synthesis Tool (JIST) is an example of that work. JIST is a set of automated tools and techniques to synthesize interfaces to Java modules.
Given a Java class file F that offers a set of method calls M, an interface to F is a small set of rules that capture the correct sequences of calls of methods in M. For example, if F is a file-manipulation program, the correct interface could be the set of sequences:
open. (read)*. close
The JIST tool extracts a small interface for a Java class automatically using Boolean abstraction of Java byte code, followed by the solution of games over the Boolean model using state-space exploration heuristics (BDDs, SAT solvers, and so forth).