Alloy*: a general-purpose higher-order relational constraint solver. (English) Zbl 1425.68264

Summary: 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.


68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI Link


[1] Alloy* home page. http://alloy.mit.edu/alloy/hola
[2] Aigner, Martin; Ziegler, Günter M., Turán’s graph theorem, 183-187 (2001), Berlin, Heidelberg
[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, Jasmin Christian; Nipkow, Tobias, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, 131-146 (2010), Berlin, Heidelberg · Zbl 1291.68326
[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 · Zbl 1213.68578
[12] Dennis G (2009) A relational framework for bounded program verification. PhD thesis, MIT
[13] Erdos, P.; Renyi, A., On the evolution of random graphs, Math Inst Hung Acad Sci, 5, 17-61 (1960) · Zbl 0103.16301
[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 · Zbl 1242.68280
[18] Gulwani, S.; Harris, WR; Singh, R., Spreadsheet data manipulation using examples, Commun ACM, 55, 97-105 (2012)
[19] Hughes, G.; Bultan, T., Automated verification of access control policies using a sat solver, STTT, 10, 503-520 (2008)
[20] Jackson D (2006) Software abstractions: logic, language, and analysis. MIT Press, Cambridge
[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 · Zbl 1253.68095
[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, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare, Model Finding for Recursive Functions in SMT, 133-151 (2016), Cham · Zbl 1475.68448
[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 · Zbl 1186.68304
[56] Vaziri, Mandana; Jackson, Daniel, Checking Properties of Heap-Manipulating Procedures with a Constraint Solver, 505-520 (2003), Berlin, Heidelberg · Zbl 1031.68518
[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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.