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

Article

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.

Keywords

Alloy Model finding Higher-order logic Synthesis Design 

Notes

Acknowledgements

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

References

  1. 1.
  2. 2.
    Aigner M, Ziegler GM (2001) Turán’s graph theorem. In: Proofs from THE BOOK. Springer, Berlin, pp 183–187Google Scholar
  3. 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–17Google Scholar
  4. 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. 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 1Google Scholar
  6. 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–387Google Scholar
  7. 7.
    Bjørner N, McMillan K, Rybalchenko A (2012) Program verification as satisfiability modulo theories. In: SMT workshop at IJCAR, vol 20Google Scholar
  8. 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–146Google Scholar
  9. 9.
    Boyatt R, Sinclair J (2008) Experiences of teaching a lightweight formal method. Electronic Notes in Theoretical Computer Science, pp 71–80Google Scholar
  10. 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–311Google Scholar
  11. 11.
    De Moura L, Bjørner N (2007) Efficient e-matching for SMT solvers. In: Automated deduction—CADE-21. Springer, pp 183–198Google Scholar
  12. 12.
    Dennis G (2009) A relational framework for bounded program verification. PhD thesis, MITGoogle Scholar
  13. 13.
    Erdos P, Renyi A (1960) On the evolution of random graphs. Math Inst Hung Acad Sci 5:17–61MathSciNetMATHGoogle Scholar
  14. 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–69Google Scholar
  15. 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–205Google Scholar
  16. 16.
    Galeotti JP, Rosner N, López Pombo CG, Frias MF (2010) Analysis of invariants for efficient bounded verification. In: ISSTA. ACM, pp 25–36Google Scholar
  17. 17.
    Ge Y, De Moura L (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Computer aided verification. Springer, pp 306–320Google Scholar
  18. 18.
    Gulwani S, Harris WR, Singh R (2012) Spreadsheet data manipulation using examples. Commun ACM 55(8):97–105CrossRefGoogle Scholar
  19. 19.
    Hughes G, Bultan T (2008) Automated verification of access control policies using a sat solver. STTT 10(6):503–520CrossRefGoogle Scholar
  20. 20.
    Jackson D (2006) Software abstractions: logic, language, and analysis. MIT Press, CambridgeGoogle Scholar
  21. 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–224Google Scholar
  22. 22.
    Jhala R, Majumdar R, Rybalchenko A (2011) HMC: verifying functional programs using abstract interpreters. In: Computer aided verification. Springer, pp 470–485Google Scholar
  23. 23.
    Köksal AS, Kuncak V, Suter P (2010) Constraints as control. In: ACM SIGPLAN NoticesGoogle Scholar
  24. 24.
    Kuncak V, Jackson D (2005) Relational analysis of algebraic datatypes. In: ACM SIGSOFT software engineering notes, vol 30. ACM, pp 207–216Google Scholar
  25. 25.
    Kuncak V, Mayer M, Piskac R, Suter P (2010) Comfusy: a tool for complete functional synthesis. In: CAV, pp 430–433Google Scholar
  26. 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–158Google Scholar
  27. 27.
    Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: LPAR-16, LNCS, vol 6355. Springer, pp 348–370Google Scholar
  28. 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–430Google Scholar
  29. 29.
    Leino KRM, Moskal M (2013) Co-induction simply: automatic co-inductive proofs in a program verifier. Technical report, MSR-TR-2013-49, Microsoft ResearchGoogle Scholar
  30. 30.
    Marinov D, Khurshid S (2001) Testera: a novel framework for automated testing of java programs. In: Automated software engineering. IEEE, pp 22–31Google Scholar
  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–71Google Scholar
  32. 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. 33.
    Milicevic A, Rayside D, Yessenov K, Jackson D (2011) Unifying execution of imperative and declarative code. In: ICSE, pp 511–520Google Scholar
  34. 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–323Google Scholar
  35. 35.
    de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS 2008, LNCS, vol 4963. Springer, pp 337–340Google Scholar
  36. 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–110Google Scholar
  37. 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 60Google Scholar
  38. 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–958Google Scholar
  39. 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–8Google Scholar
  40. 40.
    Nelson T, Saghafi S, Dougherty DJ, Fisler K, Krishnamurthi S (2013) Aluminum: principled scenario exploration through minimality. In: ICSE. IEEE Press, pp 232–241Google Scholar
  41. 41.
    Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL—a proof assistant for higher-order logic, Lecture notes in computer science, vol 2283. SpringerGoogle Scholar
  42. 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–40Google Scholar
  43. 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–151Google Scholar
  44. 44.
    Rondon PM, Kawaguci M, Jhala R (2008) Liquid types. In: ACM SIGPLAN Notices, vol 43. ACM, pp 159–169Google Scholar
  45. 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–33Google Scholar
  46. 46.
    Samimi H, Aung ED, Millstein TD (2010) Falling back on executable specifications. In: ECOOP, pp 552–576Google Scholar
  47. 47.
    Schaad A, Moffett JD (2002) A lightweight approach to specification and analysis of role-based access control extensions. In: SACMAT, pp 13–22Google Scholar
  48. 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–26Google Scholar
  49. 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–299Google Scholar
  50. 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–415Google Scholar
  51. 51.
    Srivastava S, Gulwani S, Chaudhuri S, Foster JS (2011) Path-based inductive synthesis for program inversion. In: PLDI 2011. ACM, pp 492–503Google Scholar
  52. 52.
  53. 53.
    Torlak E (2008) A constraint solver for software engineering: finding models and cores of large relational specifications. PhD thesis, MITGoogle Scholar
  54. 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–152Google Scholar
  55. 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–647Google Scholar
  56. 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–520Google Scholar
  57. 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–96Google Scholar

Copyright information

© Springer Science+Business Media New York 2017

Authors and Affiliations

  1. 1.Massachusetts Institute of TechnologyCambridgeUSA
  2. 2.University of CaliforniaBerkeleyUSA
  3. 3.MicrosoftCambridgeUSA

Personalised recommendations