Research at Automated Software Design Group

 .

The focus of our research is on problems at the intersection of Software Engineering, Dependable Distributed Computing, and Formal Methods. In the past decade, we have been concentrated on the problem of automated synthesis of fault-tolerant distributed programs. Specifically, we have developed algorithms and software tools that automatically generate self-stabilizing system, where a self-stabilizing system recovers from any configuration/state to a set of legitimate states and behaviors, and remains there as long as no faults perturb it. This is a significant problem as numerous systems (e.g., autonomous robots/vehicles, IoT, network protocols) are managed and controlled by distributed programs that might be subject to transient faults (e.g., soft errors, bad initialization, loss of coordination). As such, the correctness of such systems is of utmost importance.

In another joint project with researchers at NASA Langley’s Formal Methods group, we have developed a mechanically-verified framework in the PVS theorem prover for Riemann Integral. This is a high-impact problem as real-valued functions have applications in numerous scientific and engineering fields (e.g., avionics). Our contributions in this project have been integrated in NASA Langley’s PVS library.