Current
-
Forge: A Tool and Language for Teaching Formal Methods
Forge is a lightweight formal-methods tool, similar to Alloy 6, built with teaching in mind. Forge provides a progression of sub-languages that gradually build in expressive power to match students' experience and expertise.
Older Projects
-
Flowlog, a tierless programming language for software-defined networks.
Read more about Flowlog in our papers, or in our
blog posts on the topic.
Download Flowlog here.
-
The Margrave Tool for Policy Analysis
Margrave provides concrete scenarios that illustrate how
security policies behave and interact. One might ask Margrave how
packets are handled differently by different paths through a network,
or use it to discover which policy rules contribute to that
difference.
Margrave supports several real-world policy languages, as well as its
own intermediate policy language, and provides a flexible query
language for users interested in verifying properties or in narrowing
the scope of scenarios given.
For more information,
visit The Margrave Project Homepage.
-
Aluminum
Aluminum is a modification of
the Alloy Analyzer that
presents only minimal models: those in which every fact is
necessary. Aluminum also lets users explore the scenario space for a
specification by augmenting a given model with consistent facts; the
resulting minimal models illustrate the consequences of such
additions.
Aluminum is available for download here.