Symbolic Alloy

J. H. Siddiqui and S. Khurshid
International Conference on Formal Engineering Methods (ICFEM 2011)

Abstract

Symbolic execution is a technique for systematic exploration of program behaviors using symbolic inputs, which characterize classes of concrete inputs. Symbolic execution is traditionally performed on im- perative programs, such as those in C/C++ or Java. This paper presents a novel approach to symbolic execution for declarative programs, specif- ically those written in Alloy – a first-order, declarative language based on relations. Unlike imperative programs that describe how to perform computation to conform to desired behavioral properties, declarative pro- grams describe what the desired properties are, without enforcing a spe- cific method for computation. Thus, symbolic execution does not directly apply to declarative programs the way it applies to imperative programs. Our insight is that we can leverage the fully automatic, SAT-based anal- ysis of the Alloy Analyzer to enable symbolic execution of Alloy models – the analyzer generates instances, i.e., valuations for the relations in the model, that satisfy the given properties and thus provides an exe- cution engine for declarative programs. We define symbolic types and operations, which allow the existing Alloy tool-set to perform symbolic execution for the supported types and operations. We demonstrate the efficacy of our approach using a suite of models that represent struc- turally complex properties. Our approach opens promising avenues for new forms of more efficient and effective analyses of Alloy models.
(ICFEM 2011), Durham, United Kingdom, October 2011. (Acceptance rate: 30%, 31/103)

BibTex

@inproceedings { icfem2011,
author = { }, }