Alloy*: Higher-Order Extension to Alloy

The last decade has seen a dramatic growth in the use of constraint solvers as a computational mechanism, not only for analysis of software, but also at runtime. Solvers are available for a variety of logics but are generally restricted to first-order formulas. Some tasks, however, most notably those involving synthesis, are inherently higher order;…

Sterling: An Alloy Visualizer

Sterling combines Alloy with web-based visualizations, providing both basic Alloy visualization capabilities and a robust platform for the development of domain specific visualizations of Alloy instances. The idea for a new visualization platform was born from the need to create domain-specific visualizations for models in the field of scientific computing, such as those used to…

A Repair Framework for Alloy

ARepair is a command line tool built on top of Alloy4.2. Given a faulty Alloy model (potentially with multiple faults) and a set of AUnit tests that capture the desired model properties, ARepair is able to repair the model so that all AUnit tests. Internally, ARepair has three main components: a fault locator that is…

ASketch: A Sketching Framework for Alloy

ASketch is a command line tool built on top of Alloy5.0. Given a partial Alloy model, a candidate fragment generator, and a set of AUnit tests that capture the desired model properties, ASketch is able to fill holes with the corresponding candidate fragments and makes the completed model satisfy all AUnit tests. Internally, ASketch automatically…

SERL’s Equals Checker

EQ is a static analysis tool for checking problems related to the Object.equals(Object) method in Java. It works in two layers: 1. Low level error detection through path-sensitive data flow analyses 2. High level semantic errors through a constraint solver The path-sensitive, inter-procedural analysis framework is built on top of Soot which forms the basis…

Margrave Policy Analyzer

Modern computing systems are teeming with policies. Errors in policies can be embarassing, costly, and have legal consequences. But making mistakes is easy! Policies may be geographically distributed, encode complex dependencies, and interact with environments that change frequently. Enforcing an organization’s security goals may require the cooperation of several policies in different languages and at…

Echo

Echo is a tool for model repair and transformation built over the Alloy model finder, with support for bidirectional model transformations. It is able to both check and recover, through minimal updates, both intra- and inter-model consistency, and is deployed over the Eclipse Modeling Framework (EMF).