Alloy is a declarative language for lightweight modelling and analysis of software. The core of the language is based on first-order relational logic, which offers an attractive balance between analysability and expressiveness. The logic is expressive enough to capture the intricacies of real systems, but is also simple enough to support fully automated analysis with the Alloy Analyzer. The Analyzer is built on a SAT-based constraint solver and provides automated simulation, checking and debugging of Alloy specifications. Because of its automated analysis and expressive logic, Alloy has been applied in a wide variety of domains. These applications have motivated a number of extensions both to the Alloy language and to its SAT-based analysis. This paper provides an overview of Alloy in the context of its three largest application domains, lightweight modelling, bounded code verification and test-case generation, and three recent application-driven extensions, an imperative extension to the language, a compiler to executable code and a proof-capable analyser based on SMT.

We present a novel approach to bounded program verification that exploits recent advances of SMT solvers in modular checking of object-oriented code against its full specification. Bounded program verification techniques exhaustively check the specifications of a bounded program with respect to a bounded domain. To our knowledge, however, those techniques that target data-structure-rich programs reduce the problem to propositional logic directly, and use a SAT solver as the backend engine. Scalability, therefore, becomes a major issue due to bit blasting problems. In this paper, we present a novel approach that translates bounded Java programs and their JML specifications to quantified bit-vector formulas (QBVF) with arrays, and solves them using an SMT solver. QBVF allows logical constraints that are structurally closer to the original program and specification, and can be significantly simplified via high-level reasonings before being flattened in a basic logic. We also present a case study on a large-scale implementation of Dijkstra's shortest path algorithm. The results indicate that our approach provides significant speedups over a SAT-based approach.

A method for extracting syntactic specifications from heapmanipulating code is described. The state of the heap is represented as an environment mapping each variable or field to a relational expression. A procedure is executed symbolically, obtaining an environment for the post-state that gives the value of each variable and field in terms of the values of variables and fields of the pre-state. Approximation is introduced by forming relational unions at merge points in the control flow graph, and by widening union-of-join expressions to transitive closures. The resulting analysis is linear in the length of the code and the number of fields, but capable of producing non-trivial specifications of surprising accuracy.

Declarative models, in which conjunction and negation are freely used, are susceptible to unintentional overconstraint. Core extraction is a new analysis that mitigates this problem in the context of a checker based on reduction to SAT (systems analysis tools). It exploits a recently developed facility of SAT solvers that provides an "unsatisfiable core" of an unsatisfiable set of clauses, often much smaller than the clause set as a whole. The unsatisfiable core is mapped back into the syntax of the original model, showing the user fragments of the model found to be irrelevant. This information can be a great help in discovering and localizing overconstraint, and in some cases pinpoints it immediately. The construction of the mapping is given for a generalized modeling language, along with a justification of the soundness of the claim that the marked portions of the model are irrelevant. Experiences in applying core extraction to a variety of existing models are discussed.