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:
Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Equivalence-Based Abstraction Refinement for \(\mu \)HORS Model Checking

verfasst von : Xin Li, Naoki Kobayashi

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Kobayashi and Igarashi proposed model checking of \(\mu \)HORS (recursively-typed higher-order recursion schemes), by which a wide range of programs such as object-oriented programs and multi-threaded programs can be precisely modeled and verified. In this work, we present a procedure for \(\mu \)HORS model checking that improves the procedure based on automata-based abstraction refinement proposed by Kobayashi and Li. The new procedure optimizes each step of the abstract-check-refine paradigm of the previous procedure. Specially, it combines the strengths of automata-based and type-based abstraction refinement as equivalence-based abstraction refinement. We have implemented the new procedure, and confirmed that it always outperformed the original automata-based procedure on runtime efficiency, and successfully verified all benchmarks which were previously impossible.

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 Observational Refinement and Merge for Disjunctive MTSs
Nächstes Kapitel Greener Bits: Formal Analysis of Demand Response
Fußnoten
1
Note that, the choice of \(\mathcal {B}_0\) would not affect relative completeness but practical efficiency of the procedure. An interested reader may wish to consult [8] for some approaches to constructing \(\mathcal {B}_0\).
 
2
It does not change the graph structure by doing so, because the arguments of \(B\) occurring in the reduction could never be merged according to the assumption on \(\sim \).
 
Literatur
1.
Aehlig, K.: A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods Comput. Sci. 3(3), 1–23 (2007)MathSciNetCrossRefMATH
2.
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15(4), 575–631 (1993)CrossRef
3.
Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Rocca, S.R.D. (ed.) CSL 2013. LIPIcs, vol. 23, pp. 129–148. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)
4.
5.
Knapik, T., Niwiński, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)CrossRef
6.
7.
Kobayashi, N., Igarashi, A.: Model-checking higher-order programs with recursive types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 431–450. Springer, Heidelberg (2013)CrossRef
8.
Kobayashi, N., Li, X.: Automata-based abstraction refinement for \(\rm \mu \)HORS model checking. In: Proceedings of LICS 2015, pp. 713–724. IEEE Computer Society (2015)
9.
Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: Proceedings of LICS 2009, pp. 179–188. IEEE Computer Society Press (2009)
10.
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) PLDI 2011, pp. 222–233. ACM (2011)
11.
Li, X., Kobayashi, N.: Equivalence-based abstraction refinement for \(\rm \mu \)HORS model checking. Full version, available from the first author’s web page (2016)
12.
Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81–90. IEEE Computer Society Press (2006)
13.
Ong, C.H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Ball, T., Sagiv, M. (eds.) POPL 2011, pp. 587–598. ACM Press (2011)
14.
Ramsay, S., Neatherway, R., Ong, C.H.L.: An abstraction refinement approach to higher-order model checking. In: Jagannathan, S., Sewell, P. (eds.) POPL 2014. ACM (2014)
Metadaten
Titel
Equivalence-Based Abstraction Refinement for HORS Model Checking
verfasst von
Xin Li
Naoki Kobayashi
Copyright-Jahr
2016
Buch
Automated Technology for Verification and Analysis

Print ISBN: 978-3-319-46519-7

Electronic ISBN: 978-3-319-46520-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46520-3_20