Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 1/2019

27.01.2017

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

verfasst von: Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang, Daniel Jackson

Erschienen in: Formal Methods in System Design | Ausgabe 1/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Nächster Artikel Exploiting partial variable assignment in interpolation-based model checking

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
The expression https://static-content.springer.com/image/art%3A10.1007%2Fs10703-016-0267-2/MediaObjects/10703_2016_267_IEq21_HTML.gif corresponds to the transpose of relation https://static-content.springer.com/image/art%3A10.1007%2Fs10703-016-0267-2/MediaObjects/10703_2016_267_IEq22_HTML.gif; (https://static-content.springer.com/image/art%3A10.1007%2Fs10703-016-0267-2/MediaObjects/10703_2016_267_IEq23_HTML.gif) evaluates to true if and only if https://static-content.springer.com/image/art%3A10.1007%2Fs10703-016-0267-2/MediaObjects/10703_2016_267_IEq24_HTML.gif is a subset of https://static-content.springer.com/image/art%3A10.1007%2Fs10703-016-0267-2/MediaObjects/10703_2016_267_IEq25_HTML.gif; https://static-content.springer.com/image/art%3A10.1007%2Fs10703-016-0267-2/MediaObjects/10703_2016_267_IEq26_HTML.gif is a built-in relation that maps every element to itself, and; https://static-content.springer.com/image/art%3A10.1007%2Fs10703-016-0267-2/MediaObjects/10703_2016_267_IEq27_HTML.gif 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.
 
Literatur
1.
2.
Aigner M, Ziegler GM (2001) Turán’s graph theorem. In: Proofs from THE BOOK. Springer, Berlin, pp 183–187CrossRef
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.
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–146CrossRef
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.
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–105CrossRef
19.
Hughes G, Bultan T (2008) Automated verification of access control policies using a sat solver. STTT 10(6):503–520CrossRef
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
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.
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–151CrossRef
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.
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–520CrossRef
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
Metadaten
Titel
Alloy*: a general-purpose higher-order relational constraint solver
verfasst von
Aleksandar Milicevic
Joseph P. Near
Eunsuk Kang
Daniel Jackson
Publikationsdatum
27.01.2017
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 1/2019
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-016-0267-2

Premium Partner

    Bildnachweise