Alloy: a lightweight object modelling notation

By Daniel Jackson. TSEM, 2002

1,420 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, Signal Processing

View Paper: https://www.semanticscholar.org/paper/aa4d8e35fa6cfd8946075a1c24778cfa99bc24f7

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Signal Processing

Citations in the corpus

Optimizing database-backed applications with query synthesis (2013, background): “There are many prior work in modeling relational operations, for instance using bags [9], sets [22], and nested relational calculus [39].”
ProB: A Model Checker for B (2003, methodology): “Our constraint-based checker is strongly related to the alloy analyzer developed by Jackson [18, 19]. alloy is a special purpose lightweight object language which does not have the same penetration as B, but is well suited to constraint checking.”
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints (2007, methodology): “For example, several model-checking systems take problems specified in expressive firstorder logics such as Alloy [22] and the CLU logic [9] and encode them as Boolean CNF instances that are passed on to standard SAT solvers.”
A survey of autonomic computing—degrees, models, and applications (2008, methodology): “Further, the Allow object modeling notation [Jackson 2002] has been applied to Darwin components to be able to specify constraints on the components [Georgiadis et al. 2002].”
Self-organising software architectures for distributed systems (2002, background): “In section 2, we address the problem of ensuring that the architecture specification constrains the system to have the required set of structures.”
TestEra: a novel framework for automated testing of Java programs (2001, methodology): “We performed the actual analyses on specifications written in Alloy-Alpha [13] and available at http://www.”
Software Abstractions - Logic, Language, and Analysis (2006, background): “An exact correspondence between textual and diagrammatic forms was a design goal of an earlier version of Alloy [33], but was lost when signatures were introduced.”
Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications (2003, methodology): “This unsatisfiable core is useful in some applications such as debugging software models in the Alloy system [17], FPGA routing [2] and AI planning.”
Alcoa: the Alloy constraint analyzer (2000, background): “Its input language, Alloy [8], is close enough to UML to make a transcription of an object model diagram into Alloy a trivial task, and close enough to Z and VDM to make many existing specifications amenable to automatic analysis for the first time.”