Mana Taghdiri

Many high-level, safety properties of software systems can be specified declaratively as a set of constraints expressed in Alloy -- a first-order relational logic. Alloy has been widely used in academia and industry for verifying network protocols, schedulers, file systems, medical devices, and for program analysis.

The Alloy Analyzer is a fully automatic tool for checking properties and simulating Alloy models. It works by translating the Alloy formulas to a Boolean satisfiability (SAT) problem, and using a SAT solver as the backend engine. This analysis is performed with respect to a user-defined finite scope; only a finite number of values is allowed for each type.

In this project, we improve scalability of Alloy, i.e. help it check properties of bigger systems, by using a special kind of SAT solver that consults a user-provided API to detect conflicts faster. The task of this project is to design and implement such an API for the special domain of Alloy problems. The project will be guided by concrete examples. It is a collaborative project with Dr. Vijay Ganesh from MIT.

Requirements:

• Strong background in first-order Logic is necessary.
• Experience in Java and/or C++ is also necessary.

If interested, please contact mana.taghdiri@kit.edu