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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Use of the Modified EPSILON Decomposition for the LTI Models Reduction Kapitel lesen Erstes Kapitel lesen

2018 | Supplement | Buchkapitel

Formalization of the Nominative Algorithmic Algebra in Mizar

verfasst von : Artur Korniłowicz, Andrii Kryvolap, Mykola Nikitchenko, Ievgen Ivanov

Erschienen in: Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology – ISAT 2017

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We describe a formalization of the nominative algorithmic algebra in the Mizar proof assistant. This algebra is a generalization of Glushkov algorithmic algebras which is well suited for representing semantics and specifying properties of programs on complex data structures which interact with external environment in convenient and unified way. We describe formal definitions and formally proven and checked statements about the carrier sets and operations (program compositions) of this algebra. The obtained results are useful for implementing methods of automated verification of software, for example, for the Internet of Things (IoT) and ensuring safety of IoT systems.

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 Towards Standardized Mizar Environments
Nächstes Kapitel Military and Crisis Management Decision Support Tools for Situation Awareness Development Using Sensor Data Fusion
Literatur
1.
2.
Wiedijk, F. (ed.): The Seventeen Provers of the World. Lecture Notes in Artificial Intelligence, vol. 3600. Springer, Heidelberg (2006)
3.
4.
5.
6.
CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: OSDI 2016 Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, Savannah, GA, USA, 2–4 November 2016 (2016)
7.
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)CrossRefMATH
8.
9.
Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: An approach to formalization of an extension of Floyd-Hoare logic. In: Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer (ICTERI 2017), Kyiv, Ukraine, 15–18 May 2017. CEUR-WS.org (2017). http://​ceur-ws.​org/​Vol-1844/​10000504.​pdf
10.
Nikitchenko, N.S.: A composition nominative approach to program semantics, IT-TR 1998-020. Technical report, Technical University of Denmark (1998)
11.
Glushkov, V.: Automata theory and formal transformations of microprograms. Cybernetics 5, 3–10 (1965). (in Russian)CrossRef
12.
Floyd, R.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol. 19, pp. 19–32 (1967)
13.
14.
Nikitchenko, M., Shkilniak, S.: Algebras and logics of partial quasiary predicates. Algebra Discret. Math. 23(2), 263–278 (2017)
15.
16.
17.
Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the algebra of nominative data in Mizar. In: 2017 Federated Conference on Computer Science and Information Systems (2017, accepted)
18.
Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K., Urban, J.: Mizar: state-of-the-art and beyond. In: Intelligent Computer Mathematics – International Conference, CICM 2015, Proceedings, Washington, DC, USA, pp. 261–279 (2015). http://​dx.​doi.​org/​10.​1007/​978-3-319-20615-8_​17
19.
Grabowski, A., Korniłowicz, A., Schwarzweller, C.: Equality in computer proof assistants. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2015 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 5, pp. 45–54. IEEE (2015). http://​dx.​doi.​org/​10.​15439/​2015F229
20.
Byliński, C.: Partial functions. Formaliz. Math. 1(2), 357–367 (1990)
21.
Byliński, C.: Some basic properties of sets. Formaliz. Math. 1(1), 47–53 (1990)
22.
Bancerek, G., Trybulec, A.: Miscellaneous facts about functions. Formaliz. Math. 5(4), 485–492 (1996)
Metadaten
Titel
Formalization of the Nominative Algorithmic Algebra in Mizar
verfasst von
Artur Korniłowicz
Andrii Kryvolap
Mykola Nikitchenko
Ievgen Ivanov
Copyright-Jahr
2018
Buch
Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology – ISAT 2017

Print ISBN: 978-3-319-67228-1

Electronic ISBN: 978-3-319-67229-8

Copyright-Jahr: 2018

DOI
https://doi.org/10.1007/978-3-319-67229-8_16

Premium Partner

    Bildnachweise