Mana Taghdiri

Many high-level properties of software systems can be specified declaratively as a set of constraints expressed in a first-order relational logic. Safety properties of systems, in particular, have been successfully expressed in Alloy, a modeling language developed by MIT’s Software Design Group. 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 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.

The task of this thesis project is to design and implement a set of optimizations on top of the Alloy Analyzer that allows Alloy models to be checked with respect to bigger domains. The optimizations will be both at the Alloy level (based on theories of quantifiers, equality, and set theory) and at the SAT level to leverage existing parallel SAT solvers. The project will be guided by a few concrete case studies.

Strong background in first-order Logic is necessary. Experience in Java, C++, and/or Perl programming will become very useful.

This thesis is a joint project with MIT. It will be mainly supervised by Juniorprof. Mana Taghdiri (from KIT, Automated Software Analysis Group), and co-supervised by Dr. Vijay Ganesh (from MIT).

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