Projects

Current Active Projects:

Live Programming for Formal Methods

Current model development environments are rather “bare bones”, providing no guidance or feedback other than the output itself, and limiting the revision process to the age-old “edit and check”. We are exploring how to combine live programming innovations with the strengths inherent to modeling languages to provide a range of contextualized feedback during the development of software models. For instance, code completion is a common modern IDE feature that does not currently exist for modeling languages. We are exploring how to provide relevant and meaningful formula completion suggestions as the user types their model.

Verified Workflows Using LLMs to Develop Code

AI-assisted software development, and agentic coding in particular, has sharply increased the rate at which software engineers produce code. While features are developed and deployed more rapidly, the bottleneck in the software development life cycle moves from writing code to verifying its correctness. One way to ensure that the right code is being created is to leverage software models. This work explores the ways in which we can leveraging formal specifications to help guide LLM-assisted code development and verify the output.

Verification of AI Systems

Machine learning is a popular, growing field. However, machine learning systems are very different in nature to our previous definitions of software programs. As we start to integrate machine learning systems into our daily lives, there is a pressing need to make sure these systems are correct.