Skip to main content
SpringerLink
Log in

Alloy*: a general-purpose higher-order relational constraint solver

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

The last decade has seen a dramatic growth in the use of constraint solvers as a computational mechanism, not only for analysis of software, but also at runtime. Solvers are available for a variety of logics but are generally restricted to first-order formulas. Some tasks, however, most notably those involving synthesis, are inherently higher order; these are typically handled by embedding a first-order solver (such as a SAT or SMT solver) in a domain-specific algorithm. Using strategies similar to those used in such algorithms, we show how to extend a first-order solver (in this case Kodkod, a model finder for relational logic used as the engine of the Alloy Analyzer) so that it can handle quantifications over higher-order structures. The resulting solver is sufficiently general that it can be applied to a range of problems; it is higher order, so that it can be applied directly, without embedding in another algorithm; and it performs well enough to be competitive with specialized tools. Just as the identification of first-order solvers as reusable backends advanced the performance of specialized tools and simplified their architecture, factoring out higher-order solvers may bring similar benefits to a new class of tools.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

Notes

  1. The expression corresponds to the transpose of relation ; () evaluates to true if and only if is a subset of ; is a built-in relation that maps every element to itself, and; returns the intersection of the two relations.

  2. For linear arithmetics and Boolean operators listed in Fig. 8, our evaluation procedure employs corresponding built-in operators in Alloy. Since they have the standard semantics, we omit their definitions.

  3. For max clique and max independent set, we used the Bron–Kerbosch heuristic algorithm; for the other two, no good heuristic algorithm is known, and so we implemented enumerative search. In both cases, we used Java.

  4. If we first rewrote Turán’s theorem to use domain constraints, there would be no nested CEGIS loops left, so increments would be first-order even without the other optimization.

References

  1. Alloy* home page. http://alloy.mit.edu/alloy/hola

  2. Aigner M, Ziegler GM (2001) Turán’s graph theorem. In: Proofs from THE BOOK. Springer, Berlin, pp 183–187

    Chapter  Google Scholar 

  3. Alur R, Bodík R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD. IEEE, pp 1–17

  4. Alur R, Bodík R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2014) Syntax-guided synthesis competition report (2014). http://sygus.seas.upenn.edu/files/sygus_extended

  5. Alvaro P, Hutchinson A, Conway N, Marczak WR, Hellerstein JM (2012) Bloomunit: declarative testing for distributed programs. In: Proceedings of the fifth international workshop on testing database systems, DBTest 2012, Scottsdale, AZ, USA, 21 May 2012, p 1

  6. Barnett M, Chang BYE, DeLine R, Jacobs B, Leino KRM (2006) Boogie: a modular reusable verifier for object-oriented programs. In: FMCO 2005, LNCS, vol 4111. Springer, pp 364–387

  7. Bjørner N, McMillan K, Rybalchenko A (2012) Program verification as satisfiability modulo theories. In: SMT workshop at IJCAR, vol 20

  8. Blanchette JC, Nipkow T (2010) Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Interactive theorem proving, first international conference, ITP 2010, Proceedings, Edinburgh, UK, 11–14 July 2010, pp 131–146

    Chapter  Google Scholar 

  9. Boyatt R, Sinclair J (2008) Experiences of teaching a lightweight formal method. Electronic Notes in Theoretical Computer Science, pp 71–80

  10. de Andrade FR, Faria JP, Lopes A, Paiva ACR (2012) Specification-driven unit test generation for java generic classes. In: Integrated formal methods—9th international conference, IFM 2012, Proceedings, Pisa, Italy, 18–21 June 2012, pp 296–311

  11. De Moura L, Bjørner N (2007) Efficient e-matching for SMT solvers. In: Automated deduction—CADE-21. Springer, pp 183–198

  12. Dennis G (2009) A relational framework for bounded program verification. PhD thesis, MIT

  13. Erdos P, Renyi A (1960) On the evolution of random graphs. Math Inst Hung Acad Sci 5:17–61

    MathSciNet  MATH  Google Scholar 

  14. Ferreira JF, Mendes A, Cunha A, Baquero C, Silva P, Barbosa LS, Oliveira JN (2011) Logic training through algorithmic problem solving. In: Tools for teaching logic. Springer, pp 62–69

  15. Fisler K, Krishnamurthi S, Meyerovich LA, Tschantz MC (2005) Verification and change-impact analysis of access-control policies. In: Proceedings of the 27th ICSE. ACM, pp 196–205

  16. Galeotti JP, Rosner N, López Pombo CG, Frias MF (2010) Analysis of invariants for efficient bounded verification. In: ISSTA. ACM, pp 25–36

  17. Ge Y, De Moura L (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Computer aided verification. Springer, pp 306–320

  18. Gulwani S, Harris WR, Singh R (2012) Spreadsheet data manipulation using examples. Commun ACM 55(8):97–105

    Article  Google Scholar 

  19. Hughes G, Bultan T (2008) Automated verification of access control policies using a sat solver. STTT 10(6):503–520

    Article  Google Scholar 

  20. Jackson D (2006) Software abstractions: logic, language, and analysis. MIT Press, Cambridge

    Google Scholar 

  21. Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: ICSE, ICSE’10. ACM, New York, pp 215–224

  22. Jhala R, Majumdar R, Rybalchenko A (2011) HMC: verifying functional programs using abstract interpreters. In: Computer aided verification. Springer, pp 470–485

  23. Köksal AS, Kuncak V, Suter P (2010) Constraints as control. In: ACM SIGPLAN Notices

  24. Kuncak V, Jackson D (2005) Relational analysis of algebraic datatypes. In: ACM SIGSOFT software engineering notes, vol 30. ACM, pp 207–216

  25. Kuncak V, Mayer M, Piskac R, Suter P (2010) Comfusy: a tool for complete functional synthesis. In: CAV, pp 430–433

  26. Kurilova D, Rayside D (2013) On the simplicity of synthesizing linked data structure operations. In: Proceedings of the 12th international conference on generative programming: concepts and experiences. ACM, pp 155–158

  27. Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: LPAR-16, LNCS, vol 6355. Springer, pp 348–370

  28. Leino KRM, Milicevic A (2012) Program extrapolation with Jennisys. In: Proceedings of the international conference on object oriented programming systems languages and applications, pp 411–430

  29. Leino KRM, Moskal M (2013) Co-induction simply: automatic co-inductive proofs in a program verifier. Technical report, MSR-TR-2013-49, Microsoft Research

  30. Marinov D, Khurshid S (2001) Testera: a novel framework for automated testing of java programs. In: Automated software engineering. IEEE, pp 22–31

  31. Milicevic A, Efrati I, Jackson D (2014) \(\alpha \)Rby—an embedding of alloy in ruby. In: Abstract state machines, alloy, B, TLA, VDM, and Z. Springer, pp 56–71

  32. Milicevic A, Near JP, Kang E, Jackson D (2014) Alloy*: a higher-order relational constraint solver. Technical report, MIT-CSAIL-TR-2014-018, Massachusetts Institute of Technology. http://hdl.handle.net/1721.1/89157

  33. Milicevic A, Rayside D, Yessenov K, Jackson D (2011) Unifying execution of imperative and declarative code. In: ICSE, pp 511–520

  34. Montaghami V, Rayside D (2014) Staged evaluation of partial instances in a relational model finder. In: Abstract state machines, alloy, B, TLA, VDM, and Z. Springer, pp 318–323

  35. de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS 2008, LNCS, vol 4963. Springer, pp 337–340

  36. Nakajima S (2014) Using alloy in introductory courses of formal methods. In: Structured object-oriented formal language and method—4th international workshop, SOFL+MSVL 2014, Revised selected papers, Luxembourg, 6 Nov 2014, pp 97–110

  37. Near JP, Jackson D (2012) Rubicon: bounded verification of web applications. In: 20th ACM SIGSOFT symposium on the foundations of software engineering (FSE-20), SIGSOFT/FSE’12, Cary, NC, USA, 11–16 Nov 2012, p 60

  38. Near JP, Jackson D (2016) Finding security bugs in web applications using a catalog of access control patterns. In: Proceedings of the 38th international conference on software engineering, ICSE 2016, Austin, TX, USA, 14–22 May 2016, pp 947–958

  39. Nelson T, Barratt C, Dougherty DJ, Fisler K, Krishnamurthi S (2010) The Margrave tool for firewall analysis. In: Proceedings of the international conference on large installation system administration, pp 1–8

  40. Nelson T, Saghafi S, Dougherty DJ, Fisler K, Krishnamurthi S (2013) Aluminum: principled scenario exploration through minimality. In: ICSE. IEEE Press, pp 232–241

  41. Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic, Lecture notes in computer science, vol 2283. Springer

  42. Rayside D, Montaghami V, Leung F, Yuen A, Xu K, Jackson D (2012) Synthesizing iterators from abstraction functions. In: Proceedings of the international conference on generative programming and component engineering, pp 31–40

  43. Reynolds A, Blanchette JC, Cruanes S, Tinelli C (2016) Model finding for recursive functions in SMT. In: Automated reasoning—8th international joint conference, IJCAR 2016, Proceedings, Coimbra, Portugal, 27 June–2 July 2016, pp 133–151

    Chapter  Google Scholar 

  44. Rondon PM, Kawaguci M, Jhala R (2008) Liquid types. In: ACM SIGPLAN Notices, vol 43. ACM, pp 159–169

  45. Rosner N, Galeotti J, Bermúdez S, Blas GM, De Rosso SP, Pizzagalli L, Zemín L, Frias MF (2013) Parallel bounded analysis in code with rich invariants by refinement of field bounds. In: ISSTA. ACM, pp 23–33

  46. Samimi H, Aung ED, Millstein TD (2010) Falling back on executable specifications. In: ECOOP, pp 552–576

  47. Schaad A, Moffett JD (2002) A lightweight approach to specification and analysis of role-based access control extensions. In: SACMAT, pp 13–22

  48. Singh R, Gulwani S, Solar-Lezama A (2013) Automated feedback generation for introductory programming assignments. In: Proceedings of the 34th PLDI. ACM, pp 15–26

  49. Singh R, Solar-Lezama A (2011) Synthesizing data structure manipulations from storyboards. In: Proceedings of the symposium on the foundations of software engineering, pp 289–299

  50. Solar-Lezama A, Tancau L, Bodik R, Seshia S, Saraswat V (2006) Combinatorial sketching for finite programs. In: Proceedings of the international conference on architectural support for programming languages and operating systems, pp 404–415

  51. Srivastava S, Gulwani S, Chaudhuri S, Foster JS (2011) Path-based inductive synthesis for program inversion. In: PLDI 2011. ACM, pp 492–503

  52. SyGuS github repository. https://github.com/rishabhs/sygus-comp14.git

  53. Torlak E (2008) A constraint solver for software engineering: finding models and cores of large relational specifications. PhD thesis, MIT

  54. Torlak E, Bodik R (2013) Growing solver-aided languages with rosette. In: Proceedings of the 2013 ACM international symposium on new ideas, new paradigms, and reflections on programming and software. ACM, pp 135–152

  55. Torlak E, Jackson D (2007) Kodkod: a relational model finder. In: Tools and algorithms for the construction and analysis of systems. Springer, pp 632–647

  56. Vaziri M, Jackson D (2003) Checking properties of heap-manipulating procedures with a constraint solver. In: 9th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2003, held as part of the joint european conferences on theory and practice of software, ETAPS 2003, Proceedings, Warsaw, Poland, 7–11 Apr 2003, pp 505–520

    Chapter  Google Scholar 

  57. Yang J, Yessenov K, Solar-Lezama A (2012) A language for automatically enforcing privacy policies. In: Proceedings of the symposium on principles of programming languages, pp 85–96

Download references

Acknowledgements

This material is based upon work partially supported by the National Science Foundation under Grant Nos. CCF-1138967, CRI-0707612, and CCF-1438982.

Author information

Authors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, MA, 02139, USA

    Daniel Jackson

  2. University of California, Berkeley, USA

    Joseph P. Near & Eunsuk Kang

  3. Microsoft, Cambridge, MA, USA

    Aleksandar Milicevic

Authors
  1. Aleksandar Milicevic
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joseph P. Near
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eunsuk Kang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Daniel Jackson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Aleksandar Milicevic, Joseph P. Near or Eunsuk Kang.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Milicevic, A., Near, J.P., Kang, E. et al. Alloy*: a general-purpose higher-order relational constraint solver. Form Methods Syst Des 55, 1–32 (2019). https://doi.org/10.1007/s10703-016-0267-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-016-0267-2

Keywords

Search

Navigation