Projects

Verification and Synthesis of Formal Methods

Modeling languages can greatly increase the reliability of software systems. Unfortunately, modeling languages are hard to develop in, which brings us to a double edge sword: the software model needs to be correct in order to actually verify the software system. We investigate techniques to both test software models (in all their declarative execution weirdness) and even synthesize key portions of the model for the user.

Testing tools for Alloy

• AUnit Analyzer: Extension to the Alloy Analyzer that provides support for AUnit (test creation, test execution, coverage).
• MuAlloy: Mutation testing tool for Alloy
• AlloyFL: Tool for automated fault localization of Alloy models.

Synthesis tools for Alloy

• 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.
• ASketch: Tool to synthesize parts of an Alloy model using sketching.

Testing Tools for Prolog

• ProFl: Tool for automated fault localization of Prolog models.

Model-Based Testing of 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. An important challenge is to link highly assured formal methods of systems to the actual implementations of those systems. We explore avenues for creating valuable output from software models, which can facilitate testing of the implementation.

Scenario Enumeration Tools for Alloy:

• HawkEye: An interactive enumerator tool for Alloy that allows users to control how the next scenario enumated by Alloy differs from the current one.
• Seabs: Tool to allow the user to guide solution enumeration for an Alloy model using abstract functions.

Testing and Verification of Machine Learning 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, but the decisions of machine learning systems are often black-box. Thus, we need to know if the decision coming out of machine learning systems are “correct.”