2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), November 11-15, 2013, Palo Alto, USA

Desktop Layout

Verification
Technical Research Track
Medtrn. II
Ranger: Parallel Analysis of Alloy Models by Range Partitioning
Nicolás Rosner, Junaid H. Siddiqui, Nazareno Aguirre, Sarfraz Khurshid, and Marcelo F. Frias
(Universidad de Buenos Aires, Argentina; LUMS School of Science and Engineering, Pakistan; Universidad Nacional de Río Cuarto, Argentina; University of Texas at Austin, USA; Instituto Tecnológico de Buenos Aires, Argentina)
Abstract: We present a novel approach for parallel analysis of models written in Alloy, a declarative extension of first-order logic based on relations. The Alloy language is supported by the fully automatic Alloy Analyzer, which translates models into propositional formulas and uses off-the-shelf SAT technology to solve them. Our key insight is that the underlying constraint satisfaction problem can be split into subproblems of lesser complexity by using ranges of candidate solutions, which partition the space of all candidate solutions. Conceptually, we define a total ordering among the candidate solutions, split this space of candidates into ranges, and let independent SAT searches take place within these ranges’ endpoints. Our tool, Ranger, embodies our insight. Experimental evaluation shows that Ranger provides substantial speedups (in several cases, superlinear ones) for a variety of hard-to-solve Alloy models, and that adding more hardware reduces analysis costs almost linearly.

Authors:


Time stamp: 2019-07-19T11:58:59+02:00