Faster SAT-Based Analysis of OO-Programs by Separation of Mutant and Non Mutant Objects

FRIAS, MARCELO FABIAN; GALEOTTI, JUAN PABLO

Portland, Oregon, USA

Workshop; First Alloy Workshop; 2006

ACM

In this article we present an optimization to the analysis of DynAlloy programs based on the distinction between mutant objects (those whose state is modified by the program) and non mutant objects. This allows us to consider smaller scopes and therefore to reduce the analysis time. The theoretical observation that the technique reduces the state space exponentially is supported by examples where a striking analysis time reduction can be observed.