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
Erschienen in:
Model Checking Algorithms for Hyperproperties (Invited Paper) Kapitel lesen Erstes Kapitel lesen

2021 | OriginalPaper | Buchkapitel

Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)

verfasst von : Andreas Humenberger, Laura Kovács

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Provably correct software is one of the key challenges in our software-driven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this paper we overview some of our results for both of these scenarios when analysing programs with loops. The class of loops we consider can be modelled by a system of linear recurrence equations with constant coefficients, called C-finite recurrences. We first describe an algorithmic approach for synthesising all polynomial equality invariants of such non-deterministic numeric single-path loops. By reverse engineering invariant synthesis, we then describe an automated method for synthesising program loops satisfying a given set of polynomial loop invariants. Our results have applications towards proving partial correctness of programs, compiler optimisation and generating number sequences from algebraic relations.

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 "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

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
Vorheriges Kapitel Model Checking Algorithms for Hyperproperties (Invited Paper)
Nächstes Kapitel Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper)
Literatur
1.
Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: CAV, pp. 934–950 (2013)
2.
Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, vol. 40, pp. 1–25. IOS Press (2015)
3.
Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)CrossRef
4.
Buchberger, B.: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J. Symbolic Comput. 41(3–4), 475–511 (2006)MathSciNetMATHCrossRef
5.
Cachera, D., Jensen, T.P., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. In: SAS, pp. 58–74 (2012)
6.
Clarke, E.M., Allen Emerson, E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, pp. 52–71 (1981)
7.
Cook, B.: Formal reasoning about the security of amazon web services. In: CAV, pp. 38–47 (2018)
8.
Cooper, K.D., Taylor Simpson, L., Vick, C.A.: Operator strength reduction. ACM Trans. Program. Lang. Syst. 23(5), 603–625 (2001)CrossRef
9.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
10.
De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS, pp. 337–340 (2008)
11.
de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: ATVA, pp. 479–494 (2016)
12.
Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD, pp. 57–64 (2015)
13.
Feng, Y., Martins, R., Bastani, O., Dillig, I.: Program synthesis using conflict-driven learning. In: PLDI, pp. 420–435 (2018)
14.
German, S.M., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Trans. Software Eng. 1(1), 68–75 (1975)CrossRef
15.
Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL, pp. 317–330 (2011)
16.
Gulwani, S.: Programming by examples: applications, algorithms, and ambiguity resolution. In: IJCAR, pp. 9–14 (2016)
17.
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)MATHCrossRef
18.
Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: On strongest algebraic program invariants. J. ACM., to appear
19.
Humenberger, A.: Algebra-based loop reasoning. Ph.D. thesis, TU Wien 2021
20.
Humenberger, A., Jaroschek, M., Kovács, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: ISSAC, pp. 221–228 (2017)
21.
Humenberger, A., Jaroschek, M., Kovács, L.: Aligator.jl - a Julia package for loop invariant generation. In: CICM, pp. 111–117 (2018)
22.
Humenberger, A., Jaroschek, M., Kovács, L.:: Invariant generation for multi-path loops with polynomial assignments. In: VMCAI, pp. 226–246 (2018)
23.
Humenberger, A., Kovács, L., Bjørner, N.: Algebra-based loop synthesis. In: iFM (2020, to appear)
24.
Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE, pp. 215–224 (2010)
25.
Kalyan, A., Mohta, A., Polozov, O., Batra, D., Jain, P., Gulwani, S.: Neural-guided deductive search for real-time program synthesis from examples. In: ICLR (2018)
26.
27.
28.
Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: PLDI, pp. 248–262 (2017)
29.
Kincaid, Z., Breck, J., Cyphert, J., Reps, T.W.: Closed forms for numerical loops. PACMPL 3(POPL), 55:1–55:29 (2019)
30.
Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. PACMPL 2(POPL), 541–5433 (2018)
31.
Kovács, L.: Reasoning algebraically about p-solvable loops. In: TACAS, pp. 249–264 (2008)
32.
Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: CAV, pp. 1–35 (2013)
33.
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. Commun. ACM 55(2), 103–111 (2012)CrossRef
34.
Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980)MATHCrossRef
35.
Müller-Olm, M., Seidl, H.: A note on Karr’s algorithm. In: ICALP, pp. 1016–1028 (2004)
36.
37.
Nye, M., Hewitt, L., Tenenbaum, J., Solar-Lezama, A.: Learning to infer program sketches. In: ICML, pp. 4861–4870 (2019)
38.
Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54–75 (2007)MathSciNetMATHCrossRef
39.
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4), 443–476 (2007)MathSciNetMATHCrossRef
40.
Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: POPL, pp. 318–329 (2004)
41.
42.
Solar-Lezama, A.: The Sketching approach to program synthesis. In: APLAS, pp. 4–13 (2009)
43.
Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313–326 (2010)
Metadaten
Titel
Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)
verfasst von
Andreas Humenberger
Laura Kovács
Copyright-Jahr
2021
Buch
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-030-67066-5

Electronic ISBN: 978-3-030-67067-2

Copyright-Jahr: 2021

DOI
https://doi.org/10.1007/978-3-030-67067-2_2