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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Trusted Mechanised Specification of JavaScript: One Year On Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation

verfasst von : Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of a quantitative loop invariant to solving constraints over program variables and unknown coefficients. Lagrange interpolation allows us to find constraints with less unknown coefficients. Counterexample-guided refinement furthermore generates linear constraints that pinpoint the desired quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative loop invariants in the experiments.

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 Fast Interpolating BMC
Literatur
1.
Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: Müller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 85–100. Springer, Heidelberg (2014)
2.
Charles, K., Hang-Chin, L.: Vandermonde determinant and Lagrange interpolation in \(\mathbb{R}^s\). In: Nonlinear and Convex Analysis: Proceedings in Honor of Ky Fan, vol. 107, p. 23. CRC Press (1987)
3.
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, 20–23 May 1975, pp. 134–183. Springer (1975)
4.
Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003) CrossRef
5.
Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005) CrossRef
6.
7.
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRef
8.
Den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a hoare like logic. Int. J. Found. Comput. Sci. 13(03), 315–340 (2002)MathSciNetCrossRefMATH
9.
Dijkstra, E.W.: A Discipline of Programming. Prentice-hall, Englewood Cliffs (1976) MATH
10.
Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. Acm Sigsam Bulletin 31(2), 2–9 (1997)MathSciNetCrossRef
11.
Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. In: Matzat, B.H., Greuel, G.-M., Hiss, G. (eds.) Algorithmic Algebra and Number Theory, pp. 221–247. Springer, Heidelberg (1999)CrossRef
12.
Eaton, J.W., Bateman, D., Hauberg, S.: GNU Octave. Network thoery, London (1997)
13.
Uslar, M., Specht, M., Rohjans, S., Trefke, J., Gonzalez, J.M.V.: Introduction. In: Uslar, M., Specht, M., Rohjans, S., Trefke, J., Gonzalez, J.M.V. (eds.) The Common Information Model CIM. POWSYS, vol. 2, pp. 3–48. Springer, Heidelberg (2012) CrossRef
14.
15.
Gretz, F., Katoen, J.-P., McIver, A.: Prinsys—on a quest for probabilistic loop invariants. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 193–208. Springer, Heidelberg (2013) CrossRef
16.
Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110–132 (2014)CrossRef
17.
Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: ACM SIGPLAN Notices, vol. 43, pp. 281–292. ACM (2008)
18.
Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262–276. Springer, Heidelberg (2009) CrossRef
19.
Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634–640. Springer, Heidelberg (2009) CrossRef
20.
Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12(10), 576–580 (1969)CrossRefMATH
21.
Kapur, D.: Automatically generating loop invariants using quantifier elimination-preliminary report. In: IMACS International Conference on Applications of Computer Algebra. Citeseer (2004)
22.
Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs: In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390–406. Springer, Heidelberg (2010) CrossRef
23.
24.
McIver, A., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Heidelberg (2006) MATH
25.
Morgan, C.: Proof rules for probabilistic loops. In: Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing. Springer Verlag. (1996)
26.
27.
28.
Saniee, K.: A simple expression for multivariate Lagrange interpolation. SIAM Undergraduate Research Online 1(1) (2008)
29.
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. ACM SIGPLAN Notices 39(1), 318–329 (2004)CrossRef
30.
Metadaten
Titel
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation
verfasst von
Yu-Fang Chen
Chih-Duo Hong
Bow-Yaw Wang
Lijun Zhang
Copyright-Jahr
2015
Buch
Computer Aided Verification

Print ISBN: 978-3-319-21689-8

Electronic ISBN: 978-3-319-21690-4

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21690-4_44

Premium Partner

    Bildnachweise