Research

"The world always seems brighter when you've just made something that wasn't there before."

~Neil Gaiman

Here, I provide a highlight view of some current projects; for more information, please read some of my papers, or contact me directly.

Tools

I am interested in applied research, and the efforts to transition research ideas into real tools to be used by the software development community.

  • ProFl: Tool for automated fault localization of Prolog models.
  • Seabs: Tool to allow the user to guide solution enumeration for an Alloy model using abstract functions.
  • AUnit Analyzer: Extension to the Alloy Analyzer that provides support for AUnit (test creation, test execution, coverage).
  • MuAlloy: Mutation testing tool for Alloy
  • ASketch: Tool to synthesize parts of an Alloy model using sketching.
  • ARepair: Tool for automated repair of Alloy models. The tool firsts performs fault localization to narrow in on the buggy portion of the model, then uses synthesis techniques to fix the model.

Research Projects

Model-Based Testing of Autonomous Systems

Formally verifying a system is the first step in ensuring system reliability. However, a crucial next step is ensuing the corresponding implementation is a faithful reproduction of the formal model. I am working with an interdisciplinary team to develop methods to link highly assured formal methods of autonomous systems to the actual implementations of those systems. Due to the many collaborators on this project, we will be able to develop these practices over operational autonomous systems in the Department of Defense.

Autonomous Vehicle Verification

Autonomous vehicles are a future technology that many expect to come to fruition. The software systems associated with autonomous vehicles will inherently be safety critical and we will need rigorous techniques to ensure these system never fail. Our work focuses on approaches leveraging formal methods to develop novel techniques to verify the design, subsystem interactions, and the underlying machine learning subsystem.

SAE-GM Autodrive Challenge    SAE-GM Autodrive Challenge

Verification and Synthesis of Formal Methods

AUnit introduces the first testing infrastructure for Alloy, namely: test case, test execution and coverage. With this infrastructure in place, we can now explore how to bring well-established imperative v&v techniques (automated test generation, fault localization, mutation testing, regression testing, etc) into the Alloy language. Additionally, AUnit enables automated repair and synthesis techniques for Alloy. These frameworks ease the burden of developing Alloy models, which is a non-trivial task. Based on the success of AUnit, we plan to explore verification and synthesis techniques for a broader range of formal modeling languages.