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:
Buchtitelbild

2017 | OriginalPaper | Buchkapitel

Reasoning About Concurrency in High-Assurance, High-Performance Software Systems

verfasst von : June Andronick

Erschienen in: Automated Deduction – CADE 26

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We describe our work in the Trustworthy Systems group at Data61 (formerly NICTA) in reasoning about concurrency in high-assurance, high-performance software systems, in which concurrency may come from three different sources: multiple cores, interrupts and application-level interleaving.

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
Nächstes Kapitel Towards Logic-Based Verification of JavaScript Programs
Literatur
1.
2.
3.
Amani, S., Andronick, J., Bortin, M., Lewis, C., Christine, R., Tuong, J.: Complx: a verification framework for concurrent imperative programs. In: Bertot, Y., Vafeiadis, V. (eds.) CPP, pp. 138–150. ACM, Paris (2017)
4.
Andronick, J., Greenaway, D., Elphinstone, K.: Towards proving security in the presence of large untrusted components. In: Huuck, R., Klein, G., Schlich, B. (eds.) SSV, p. 9. USENIX, Vancouver (2010)
5.
Andronick, J., Klein, G.: Formal system verification - extension 2, final report AOARD #FA2386-12-1-4022. Technical report, NICTA, Sydney, Australia, August 2012
6.
Andronick, J., Lewis, C., Matichuk, D., Morgan, C., Rizkallah, C.: Proof of OS scheduling behavior in the presence of interrupt-induced concurrency. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 52–68. Springer, Cham (2016). doi:10.​1007/​978-3-319-43144-4_​4 CrossRef
7.
Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: van Glabbeek, R.J., Groote, J.F., Höfner, P. (eds.) Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November 2015
8.
9.
Chen, H., Wu, X.N., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible OS kernels and device drivers. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp. 431–447. ACM, New York (2016)
10.
11.
Gu, R., Shao, Z., Chen, H., Wu, X.N., Kim, J., Sjöberg, V., Costanzo, D.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: OSDI, November 2016
12.
Heiser, G., Andronick, J., Elphinstone, K., Klein, G., Kuz, I., Ryzhyk, L.: The road to trustworthy systems. In: ACMSTC, pp. 3–10. ACM, October 2010
13.
Jones, C.B.: Tentative steps towards a development method for interfering programs. Trans. Program. Lang. Syst. 5(4), 596–619 (1983)CrossRefMATH
14.
Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. CACM 53(6), 107–115 (2010)CrossRef
15.
Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. Trans. Comput. Syst. 32(1), 2:1–2:70 (2014)
16.
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) 33rd POPL, pp. 42–54. ACM, Charleston (2006)
17.
18.
19.
20.
Peters, S., Danis, A., Elphinstone, K., Heiser, G.: For a microkernel, a big lock is fine. In: APSys, Tokyo, JP, July 2015
21.
Potts, D., Bourquin, R., Andresen, L., Andronick, J., Klein, G., Heiser, G.: Mathematically verified software kernels: raising the bar for high assurance implementations. Technical report, NICTA, Sydney, Australia, July 2014
22.
Schirmer, N.: Verification of sequential imperative programs in Isabelle/HOL. Ph.D. thesis, Technische Universität München (2006)
23.
von Tessin, M.: The clustered multikernel: an approach to formal verification of multiprocessor operating-system kernels. Ph.D. thesis, School Comp. Sci. & Engin., UNSW, Sydney, Australia, December 2013
24.
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 97–108. ACM, Nice (2007)
Metadaten
Titel
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems
verfasst von
June Andronick
Copyright-Jahr
2017
Buch
Automated Deduction – CADE 26

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

Electronic ISBN: 978-3-319-63046-5

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-63046-5_1