Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Cybersicherheit Beyond 2020! Read chapter Read first chapter

2017 | OriginalPaper | Chapter

5. Software-Verifikation

Beiträge der Münchner Forschung

Authors : Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, Martin Wirsing

Published in: 50 Jahre Universitäts-Informatik in München

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Zusammenfassung

Bei der Entwicklung von Software ist es aufgrund ihrer Komplexität erforderlich, automatisierte Verfahren zur Überprüfung der korrekten Funktion einzusetzen. Um die Integration und korrekte Zusammenarbeit verschiedener Komponenten großer Softwaresysteme sicherzustellen, entwickeln Forschergruppen an den Münchner Universitäten sowohl Modell-basierte als auch Quellcode-basierte Techniken. Als Anwendungsbereiche betrachten wir unter anderem Komponenten der Infrastruktur, autonome Systeme und service-orientierte Systeme. Wir setzen Methoden und Algorithmen ein, die den Ingenieur während der Modellierung, der Programmierung und im Releasezyklus mit automatischen Techniken zur Abstraktion, Transformation und Verifikation unterstützen.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Human Collaboration Reshaped: Applications and Perspectives
next chapter Innovationszentrum Mobiles Internet des ZD.B
Footnotes
Literature
1.
F. L. Bauer. Program development by stepwise transformations – The project CIP. Appendix: Programming languages under educational and under professional aspects. In Program Construction, International Summer School, Marktoberdorf, LNCS 69, pages 237–272. Springer, 1978. DOI: 10.​1007/​BFb0014671
2.
F. L. Bauer, R. Berghammer, M. Broy, W. Dosch, F. Geiselbrechtinger, R. Gnatz, E. Hangel, W. Hesse, B. Krieg-Brückner, A. Laut, T. Matzner, B. Möller, F. Nickl, H. Partsch, P. Pepper, K. Samelson, M. Wirsing, and H. Wössner. The Munich Project CIP, Volume I: The Wide Spectrum Language CIP-L. LNCS 183. Springer, 1985. DOI: 10.​1007/​3-540-15187-7 CrossRef
3.
F. L. Bauer, B. Möller, H. Partsch, and P. Pepper. Formal program construction by transformations – Computer-aided, Intuition-guided Programming. IEEE Trans. Software Eng., 15(2):165–180, 1989. DOI: 10.​1109/​32.​21743 MathSciNetCrossRefMATH
4.
S. S. Bauer, P. Mayer, A. Schroeder, and R. Hennicker. On weak modal compatibility, refinement, and the MIO Workbench. In Proc. TACAS, LNCS 6015, pages 175–189. Springer, 2010.
5.
6.
D. Beyer. Software verification with validation of results (Report on SV-COMP 2017). In Proc. TACAS. Springer, 2017. LNCS 10206, pages 331–349, DOI: 10.1007/978-3-662-54580-5_20
7.
D. Beyer and M. Dangl. Verification-aided debugging: An interactive web-service for exploring error witnesses. In Proc. CAV (2), LNCS 9780, pages 502–509. Springer, 2016. DOI: 10.​1007/​978-3-319-41540-6_​28
8.
D. Beyer, M. Dangl, D. Dietsch, and M. Heizmann. Correctness witnesses: Exchanging verification results between verifiers. In Proc. FSE, pages 326–337. ACM, 2016. DOI: 10.​1145/​2950290.​2950351
9.
D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, and A. Stahlbauer. Witness validation and stepwise testification across software verifiers. In Proc. FSE, pages 721–733. ACM, 2015. DOI: 10.​1145/​2786805.​2786867
10.
D. Beyer, S. Gulwani, and D. Schmidt. Combining model checking and data-flow analysis. In E. M. Clarke, T. A. Henzinger, and H. Veith, editors, Handbook on Model Checking. Springer, 2017.
11.
D. Beyer, T. A. Henzinger, and G. Théoduloz. Configurable software verification: Concretizing the convergence of model checking and program analysis. In Proc. CAV, LNCS 4590, pages 504–518. Springer, 2007. DOI: 10.​1007/​978-3-540-73368-3_​51
12.
13.
14.
D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, and P. Wendler. Precision reuse for efficient regression verification. In Proc. ESEC/FSE, pages 389–399. ACM, 2013. DOI: 10.​1145/​2491411.​2491429
15.
16.
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. CONCUR, LNCS 1243, pages 135–150. Springer, 1997.
17.
M. Broy. Towards a formal foundation of the specification and description language SDL. Formal Aspects of Computing, 3(1):21–57, 1991.CrossRefMATH
18.
M. Broy and G. Ştefănescu. The algebra of stream processing functions. Theoretical Computer Science, 258(1):99–129, 2001.MathSciNetCrossRefMATH
19.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. Logic of Programs 1981, LNCS 131, pages 52–71. Springer, 1982.
20.
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752–794, 2003.MathSciNetCrossRefMATH
21.
22.
J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst., 36(3):9, 2014.CrossRef
23.
J. Esparza, M. Hofmann, T. Nipkow, H. Seidl, DFG Graduiertenkolleg GRK 1480: Programm und Modellanalyse (PUMA), 2008-2017, 2007.
24.
R. Grabowski, M. Hofmann, and K. Li. Type-based enforcement of secure programming guidelines – Code injection prevention at SAP. In Proc. FAST, LNCS 7140, pages 182–197. Springer, 2011. DOI: 10.​1007/​978-3-642-29420-4_​12
25.
T. C. Hales, J. Harrison, S. McLaughlin, T. Nipkow, S. Obua, and R. Zumkeller. A revision of the proof of the Kepler conjecture. Discrete and Computational Geometry, 44:1–34, 2010.MathSciNetCrossRefMATH
26.
R. Hennicker, M. Bidoit, and T.-S. Dang. On synchronous and asynchronous compatibility of communicating components. In Proc. COORDINATION, LNCS 9686, pages 138–156. Springer, 2016.
27.
R. Hennicker, S. Janisch, A. Kraus, and M. Ludwig. A web-based modelling and decision support system to investigate global change and the hydrological cycle in the Upper Danube basin. In Regional Assessment of Global Change Impacts – The Project GLOWA-Danube, chapter 2, pages 19–28. Springer, 2016.CrossRef
28.
R. Hennicker, A. Klarl, and M. Wirsing. Model-checking Helena ensembles with Spin. In Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, LNCS 9200, pages 331–360. Springer, 2015.
29.
M. M. Hölzl, N. Koch, M. Puviani, M. Wirsing, and F. Zambonelli. The ensemble development life cycle and best practices for collective autonomic systems. In Software Engineering for Collective Autonomic Systems – The ASCENS Approach, LNCS 8998, pages 325–354. Springer, 2015. DOI: 10.​1007/​978-3-319-16310-9_​9
30.
31.
G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. Verified Java-Bytecode Verification. PhD thesis, Institut für Informatik, Technische Universität München, 2003.
32.
G. Klein et al. seL4: Formal verification of an operating-system kernel. Commun. ACM, 53(6):107–115, 2010.CrossRef
33.
34.
35.
M. Wirsing, A. Clark, S. Gilmore, M. Hölzl, A. Knapp, N. Koch, and A. Schroeder. Semantic-based development of service-oriented systems. In Proc. FORTE, LNCS 4229, pages 24–45. Springer, 2006.
36.
M. Wirsing and M. M. Hölzl, editors. Rigorous Software Engineering for Service-Oriented Systems – Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. LNCS 6582. Springer, 2011. DOI: 10.​1007/​978-3-642-20401-2
37.
M. Wirsing, M. M. Hölzl, N. Koch, and P. Mayer, editors. Software Engineering for Collective Autonomic Systems – The ASCENS Approach. LNCS 8998. Springer, 2015. DOI: 10.​1007/​978-3-319-16310-9
Metadata
Title
Software-Verifikation
Authors
Dirk Beyer
Rolf Hennicker
Martin Hofmann
Tobias Nipkow
Martin Wirsing
Copyright Year
2017
Publisher
Springer Berlin Heidelberg
Book
50 Jahre Universitäts-Informatik in München

Print ISBN: 978-3-662-54711-3

Electronic ISBN: 978-3-662-54712-0

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-662-54712-0_5

Premium Partner

    Image Credits