MIDAS Project

Team:

The MIDAS (Model-based Intent-Driven Adaptive Software) project is part of DARPA’s IDAS (Intent-Driven Adaptive Software) program. The goal is to improve developers’ ability and efficiency to adapt software by providing a framework and and toolkit that explicates the process that leads from requirements to implementation.

The team is developing an approach to combine Vanderbilt’s model-based development tools like WebGME with Kestrel’s APT toolkit. A major research challenge is to make APT more usable to developers without a formal methods background.

We have developed Syntheto, a formal language for formal specification and synthesis that gives access to ACL2 and APT in a way that is more familiar to general developers. The Syntheto frontend, which provides an IDE based on Visual Studio Code, is available here. The Syntheto backend, which is used by the frontend to communicate with ACL2 and APT, is available here, as part of the ACL2 community books.

Publications

Syntheto: A Surface Language for APT and ACL2
Alessandro Coglio, Eric McCarthy, Stephen Westfold, Daniel Balasubramanian, Abhishek Dubey, and Gabor Karsai
May 2022
17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2023)
{Description of a prototype language that provides a more familiar and accessible interface to APT and ACL2.}