to write it; and to Devdatta Akhawe,
Adam Barth, Peifung E. Lam, John
Mitchell, and Dawn Song, whose work
formed the basis of the example used
in the article. Thank you also to the
many members of the Alloy community who have contributed to Alloy over
1. Akhawe, D., Barth, A., Lam, P.E., Mitchell, J. and Song,
D. Towards a formal foundation of Web security. In
Proceedings of the 23rd IEEE Computer Security
Foundations Symp. Edinburgh, 2010, 290–304.
2. Alexander, C. Notes on the Synthesis of Form. Harvard
University Press, 1964.
3. Alloy Tools; http://alloytools.org.
4. Alloy Models repository; https://github.com/
5. Alloy discussion forum; https://groups.google.com/
6. Barth, A., Jackson, C., and Mitchell, J.C. Robust
defenses for cross-site request forgery. In
Proceedings of the 15th ACM Conf. on Computer and
Communications Security. ACM, 2008, 75–88.
7. Baugh, J. and Altuntas, A. Formal methods and finite
element analysis of hurricane storm surge: A case
study in software verification. Science of Computer
Programming 158 (2018), 100–121.
8. Blanchette, J. and Nipkow, T. Nitpick: A
counterexample generator for higher-order logic
based on a relational model finder. In Proceedings of
the 1st Intern. Conf. Interactive Theorem Proving. M.
Kaufmann and L. C. Paulson, eds. LNCS 6172 (2010).
9. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L. and
Hwang, L.J. Symbolic model checking: 10 states and
beyond. In Proceedings of the 5th Annual Symp. Logic
in Computer Science. (Philadelphia, PA, USA, June
4–7, 1990), 428–439.
10. Dennis, G., Chang, F. and Jackson, D. Modular
verification of code with SAT. In Proceedings of
the Intern. Symp. Software Testing and Analysis.
(Portland, ME, July 2006).
11. Dennis, G., Yessenov, K. and Jackson, D. Bounded
verification of voting software. In Proceedings of the
2nd IFIP Working Conf. Verified Software: Theories,
Tools, and Experiments. (Toronto, Canada, Oct. 2008).
12. Edwards, J., Jackson, D. and Torlak, E. A type system
for object models. In Proceedings of the 12th ACM
SIGSOF T Intern. Symp. Foundations of Software
Engineering (Newport Beach, CA, USA, Oct. 31— Nov.
6, 2004), 189–199.
13. Galeotti, J. P., Rosner, N., Lopez Pombo, C.G. and Frias,
M. F. TACO: Efficient SAT-based bounded verification
using symmetry breaking and tight bounds. IEEE
Trans. Softw. Eng. 39, 9 (Sept.2013), 1283–1307.
14. Holzmann, G.J. The Spin Model Checker: Primer and
Reference Manual, Addison Wesley, 2003.
15. Huth, M. and Ryan, M. Logic in Computer Science:
Modeling and Reasoning about Systems. Cambridge
University Press, 2004.
16. Jackson, D. Software Abstractions. MIT Press, Second
17. Jackson, D. Software Abstractions; http://
18. Jackson, D., Thomas, M. and Millett, L. I. eds. Software
For Dependable Systems: Sufficient Evidence?
Committee on Certifiably Dependable Software
Systems, Computer Science and Telecommunications
Board, Division on Engineering and Physical Sciences.
National Research Council of the National Academies.
The National Academies Press, Washington, D.C., 2007.
19. Kriens, P. JPMS, The Sequel; http://aqute.
20. Macedo, N., Brunel, J., Chemouil, D., Cunha, A. and
Kuperberg, D. Lightweight specification and analysis
of dynamic systems with rich configurations. In
Proceedings of the 24th ACM SIGSOF T Intern. Symp.
Foundations of Software Engineering (Seattle, WA,
USA, 2016), 373–383.
21. Macedo, N., Cunha, A. and Guimaraes, T. Exploring
scenario exploration. Fundamental Approaches to
Software Engineering. A. Egyed and I. Schaefer, eds.
Lecture Notes in Computer Science 9033. Springer,
22. Macedo, N., Cunha, A. and Pessoa, E. Exploiting partial
knowledge for efficient model analysis. In Proceedings
of the 15th Intern. Symp. Automated Technology for
Verification and Analysis. Springer, 2017, 344–362.
23. Meng, B., Reynolds, A., Tinelli, C., and Barrett,
C. Relational Constraint Solving in SMT. In
Proceedings of the 26th Intern. Conf. Automated
Deduction. (Gothenburg, Sweden, 2017) L. de
Moura, ed. Springer.
24. Milicevic, A., Near, J.P., Kang E. and Jackson, D. Alloy*:
A general-purpose higher-order relational constraint
solver. Formal Methods in System Design, 2017, 1–32.
25. Montaghami, V. and Rayside, D. Extending alloy with
partial instances. In Proceedings of the 3rd Intern.
Conf. Abstract State Machines, Alloy, B, VDM, and Z.
26. Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K. and
Krishnamurthi, S. The Margrave tool for firewall
analysis. In Proceedings of the 24th USENIX Large
Installation System Administration Conference (San
Jose, CA, 2010).
27. Nelson, T., Danas, N., Dougherty, D.J., and
Krishnamurthi, S. The Power of Why and Why Not:
Enriching Scenario Exploration with Provenance.
Joint European Software Engineering Conference and
ACM SIGSOF T Symposium on the Foundations of
Software Engineering, 2017.
28. Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., and
Krishnamurthi, S. Aluminum: Principled scenario
exploration through minimality. In Proceedings of the
Intern. Conf. Software Engineering, 2013.
29. Padon, O., Losa, G., Sagiv, M. and Shoham S. Paxos
made EPR: Decidable reasoning about distributed
protocols. In Proceedings of the OOPSLA 2017
30. Pernsteiner, S. et al. Investigating safety of a
radiotherapy machine using system models with
pluggable checkers. Computer Aided Verification
LNCS 9780. Springer.
31. Regis, G. et al. DynAlloy Analyzer: A tool for the
specification and analysis of Alloy models with
dynamic behaviour. In Proceedings of the 11th Joint
Meeting on Foundations of Software Engineering. ACM,
New York, NY, 2017, 969–973.
32. Spivey, J. M. The Z Notation: A Reference Manual (2nd
ed.), Prentice Hall, 1992.
33. Stoica, I. et al. Chord: A scalable peer-to-peer lookup
protocol for Internet applications. IEEE/ACM Trans.
Networking 11, 1 (2003), 17–32.
34. Torlak, E. and Jackson, D. Kodkod: A relational model
finder. In Proceedings of the 13th Intern. Conf. Tools
and Algorithms for the Construction and Analysis of
Systems (Braga, Portugal, 2007), 632–647.
35. Trippel, C., Lustig, D. and Martonosi, M.
MeltdownPrime and SpectrePrime: Automatically
Synthesized Attacks Exploiting Invalidation-Based
Coherence Protocols. Feb. 2018; arX- iv:1802.03802.
36. University of Washington. PLSE Neutrons;
37. Visser, W., Havelund, K., Brat, G., Park, S.J. and Lerda,
F. Model checking programs. Automated Software
Engineering J. 10, 2 (Apr. 2003).
38. Wallace, C. Learning Discrete Structures Interactively
with Alloy. In Proceedings of the 49th ACM Tech.
Symp. Computer Science Education (Baltimore, MD,
Feb. 21–24, 2018), 1051–1051.
39. Warmer, J.B. and Kleppe, A. G. The Object Constraint
Language: Precise Modeling with UML. Addison-Wesley, 1999.
40. Wayne, H. Personal blog; https://www.hillel-wayne.com
41. Wickerson, J, Batty, M., Sorensen, T. and
Constantinides, G.A. Automatically comparing
memory consistency models. In Proceedings of the
44th ACM SIGPLAN Symp. Principles of Programming
Languages (Paris, France, 2017), 190–204.
42. Zave, P. A practical comparison of Alloy and Spin.
Formal Aspects of Computing 27 (2015), 239–253.
43. Zave, P. Reasoning about identifier spaces: How
to make Chord correct. IEEE Trans. Software
Engineering 43, 12 (Dec. 2017), 1144–1156.
Daniel Jackson is a professor of computer science and
Associate Director of the Computer Science and Artificial
Intelligence Laboratory at the Massachusetts Institute of
Technology, Cambridge, MA, USA.
© 2019 ACM 0001-0782/19/9
Iowa has recently extended CVC4, a
leading SMT solver, with a theory of
finite relations, and has promisingly
demonstrated its application to some
Alloy problems. 23
Configurations. Many Alloy models
contain two loosely coupled parts,
one defining a configuration (say of a
network) and the other the behavior
(say of sending packets). By iterating
through configurations and analyzing
each independently, one can often
dramatically reduce analysis time. 22
In some applications, a configuration
is already fully or partially known, and
the goal is to complete the instance—
in which case searching for the configuration is a wasted effort. Kodkod,
Alloy’s engine, allows the explicit definition of a “partial instance” to support this, but in Alloy itself, this notion is not well supported (and relies
on a heuristic for extracting partial
instances from formulas in a certain
form). Researchers have therefore
proposed a language extension25 to
allow partial instances to be defined
directly in Alloy itself.
How to Try Alloy
The Alloy Analyzer3 is a free download available for Mac, Windows,
and Linux. The Alloy book16 provides
a gentle introduction to relational
logic and to the Alloy language, gives
many examples of Alloy models, and
includes a reference manual and a
comparison to other languages (both
of which are available on the book’s
website17). The Alloy community
answers questions tagged with the
keyword alloy on StackOverflow, and
hosts a discussion forum. 5 A variety of
tutorials for learning Alloy are available online too, as well as blog posts
with illustrative case studies and
examples (for example, Kriens19
and Wayne40). The model used in
this article is available (along with
its visualization theme) in the Alloy
community’s model repository. 4
I am very grateful to David Chemouil,
Alcino Cunha, Peter Kriens, Shriram
Krishnamurthi, Jay Parlar, Emina Torlak, Hillel Wayne, Pamela Zave, and
the anonymous reviewers, whose suggestions improved this article greatly;
to Moshe Vardi, who encouraged me