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.