Thesis Title: “A Novel Method For Reducing The Overhead of Titanium”

Abstract: Alloy is a software modeling language based on first-order relational logic, with an analysis engine that performs bounded verification of models. Alloy has found applications in a wide range of software engineering problems, from automated synthesis and exploration of design alternatives to the analysis of programs and test case generation. Such applications of Alloy are yet challenged by the time it takes for an analysis to run, especially given that the analysis may need to be repeated frequently. Indeed, despite its capability, the reliance of the Alloy Analyzer on a computationally heavy SAT solver means that it can take a significant amount of time to analyze models.
A recent approach, called Titanuim, significantly reduces the time it takes to analyze evolving Alloy models by leveraging the previous analysis results to narrow the revised model’s exploration space. However, to improve the analysis of evolving Alloy models, Titanium depends on the availability of the entire solution space for the prior model, which may hinder the applicability of Titanium. In this work, I present a novel approach to identify the subset of solutions from the preceding model required to improve the analysis of the subsequent evolved model, thereby significantly relieving Titanium from the expensive task of generating all satisfying model instances when it is not necessary.

Committee:
Dr. Hamid Bagheri, Advisor
Dr. Witty Srisa-an
Dr. Thanhvu Nguyen

Zoom invitation link:
https://us04web.zoom.us/j/8599258649?pwd=WEtsOFVocERTM1hyV3d5Y1ppcUJSdz09

Meeting ID: 859 925 8649
Passcode: 3aVTkT