Mana Taghdiri, Aboubakr Achraf El Ghazi

Lightweight formal methods are attractive techniques for checking correctness of high-level models of software systems. They can check whether a system satisfies its requirements fully automatically. Alloy, a first-order logic developed by MIT’s Software Design Group, is a modeling language particularly tailored for this purpose. It has been widely used in academia and industry for verifying network protocols, schedulers, file systems, and for program analysis. The Alloy Analyzer is a fully automatic tool for checking properties and simulating Alloy models. The tool, however, can perform the analysis only with respect to finite domains; unrestricted quantification is not covered.

The task of this project is to develop a new engine that analyzes Alloy models while allowing unrestricted quantification. The new engine will translate Alloy to SMT-Lib and use the Z3 SMT solver, which is also fully automatic. Our preliminary study shows that an SMT-based engine works well for many Alloy models. In this project, however, we like to develop a new, alternative translation that can potentially improve the performance of the existing engine. The translation shall only cover the core constructs of Alloy, and will be guided by a couple of concrete case studies.

Requirement: 

• Basic knowledge of first order predicate logic as, e.g., taught in the “Formal Systems” lecture.
• Familiarity with Java programming

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