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:
Effect Systems Revisited—Control-Flow Algebra and Semantics Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Enhancing Top-Down Solving with Widening and Narrowing

verfasst von : Kalmer Apinis, Helmut Seidl, Vesal Vojdani

Erschienen in: Semantics, Logics, and Calculi

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present an enhancement of the generic fixpoint algorithm TD which can deal with widening and narrowing even for non-monotonic systems of equations. In contrast to corresponding enhancements proposed for other standard fixpoint algorithms, no extra priorities on variables are required. Still, a mechanism can be devised so that occurrences of the widening/narrowing operator are inserted as well as removed dynamically.

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 Guards, Failure, and Partiality: Dijkstra’s Guarded-Command Language Formulated Topologically
Nächstes Kapitel Modal Intersection Types, Two-Level Languages, and Staged Synthesis
Literatur
1.
Amato, G., Scozzari, F.: Localizing widening and narrowing. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 25–42. Springer, Heidelberg (2013) CrossRef
2.
Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing (2015). arXiv:​1503.​00883 [cs.PL]
3.
Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a Swiss army knife for program analysis. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 157–172. Springer, Heidelberg (2012) CrossRef
4.
Apinis, K.: Frameworks for analyzing multi-threaded C, Ph.D. thesis, Institut für Informatik, Technische Universität München (2014)
5.
Apinis, K., Seidl, H., Vojdani, V.: How to combine widening and narrowing for non-monotonic systems of equations. In: 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 377–386. ACM (2013)
6.
Bourdoncle, F.: Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In: Deransart, P., Małuszyński, J. (eds.) PLILP 1990. LNCS, vol. 456. Springer, Heidelberg (1990) CrossRef
7.
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Robinet, B. (ed.) 2nd International Symposium on Programming, Paris, pp. 106–130. Dunod (1976)
8.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 238–252. ACM Press (1977)
9.
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conference on Formal Description of Programming Concepts, pp. 237–277. North-Holland (1977)
10.
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) 6th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 269–282 (1979)
11.
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: 5th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 84–96. ACM Press (1978)
12.
Fecht, C., Seidl, H.: Propagating differences: an efficient new fixpoint algorithm for distributive constraint systems. Nord. J. Comput. 5(4), 304–329 (1998)MATHMathSciNet
13.
14.
Hermenegildo, M., Puebla, G., Marriott, K., Stuckey, P.: Incremental analysis of constraint logic programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 22(2), 187–223 (2000)CrossRef
15.
Hermenegildo, M.V., Puebla, G., Bueno, F., López-García, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao System preprocessor). Sci. Comput. Program. 58(1), 115–140 (2005)MATHCrossRef
16.
Hofmann, M., Karbyshev, A., Seidl, H.: Verifying a local generic solver in Coq. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 340–355. Springer, Heidelberg (2010) CrossRef
17.
Hofmann, M., Karbyshev, A., Seidl, H.: What is a pure functional? In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 199–210. Springer, Heidelberg (2010) CrossRef
18.
Kildall, G.A.: A unified approach to global program optimization. In: ACM Symposium on Principle of Programming Languages (POPL), pp. 194–206. ACM (1973)
19.
Le Charlier, B., Van Hentenryck, P.: A universal top-down fixpoint algorithm. Technical report 92–22, Institute of Computer Science, University of Namur, Belgium (1992)
20.
Miné, A.: The octagon abstract domain. Higher-Order Symb. Comput. 19(1), 31–100 (2006)MATHCrossRef
21.
Muthukumar, K., Hermenegildo, M.: Deriving a fixpoint computation algorithm for top-down abstract interpretation of logic programs. Technical report ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759 (1990)
22.
Puebla, G., Hermenegildo, M.: Optimized algorithms for the incremental analysis of logic programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145. Springer, Heidelberg (1996) CrossRef
23.
24.
Vojdani, V.: Static data race analysis of heap-manipulating C programs, Ph.D. thesis, University of Tartu, (2010)
Metadaten
Titel
Enhancing Top-Down Solving with Widening and Narrowing
verfasst von
Kalmer Apinis
Helmut Seidl
Vesal Vojdani
Copyright-Jahr
2016
Buch
Semantics, Logics, and Calculi

Print ISBN: 978-3-319-27809-4

Electronic ISBN: 978-3-319-27810-0

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-27810-0_14

Premium Partner

    Bildnachweise