GEOMAR  Forschen  Dynamik des Ozeanbodens  Marine Geodynamik  Lehre

Lehre

Die Professoren und Wissenschaftler der Marinen Geodynamik halten im Rahmen des BSc Studiengangs Physik des Erdsystems und in den MSc Studiengängen Master of Geophysics und Master of Marine Geosciences Vorlesungen. Mehr Informationen finden Sie hierzu auf den Webseiten der Christian-Albrechts-Universität zu Kiel. Wir betreuen außerdem Abschlussarbeiten (BSc, MSc und Dr. rer. nat.). Bei Interesse wenden Sie sich bitte an den jeweiligen Dozenten oder im Zweifel an Heidrun Kopp (hkopp(at)geomar.de) oder Christian Berndt (cberndt(at)geomar.de).
UnivIS
Informationssystem der Universität Kiel © Config eG 
Semester: SS 2024 

Inf-GSoZu: Introduction to Formal Software Analysis (Inf-GSoZu) (080040)

Dozent/in
Prof. Dr. Dirk Nowotka

Angaben
Vorlesung, 4 SWS, ECTS-Studium, ECTS-Credits: 8
Unterrichtssprache Englisch
Zeit und Ort: Do 12:15 - 13:45, 14:15 - 15:45, CAP4 - R.13.1304 a (außer Do 23.5.2024); Einzeltermine am 23.5.2024 12:15 - 13:45, OS75/S3 - R.31; 23.5.2024 14:15 - 15:45, OS75/S2 - R.210
vom 14.4.2024 bis zum 14.7.2024

Inhalt
Kurzfassung: In this course we consider basic principles and techniques for the detection of errors and the certification of the absence of certain errors in software systems. The covered areas include testing, model-checking, and abstract interpretation.
Lernziele: A successful attendant of this course will gain an understanding in techniques and formal methods for error finding and proving of program properties. He or she will be able to evaluate different analysis methods and to employ them.
Lehrinhalte: The course breaks down into three parts.
Part one: Testing. A systematic approach to various aspects of testing is presented: code inspections and walk throughs, control-flow coverage, data-flow coverage, black-box and white-box testing, test suites, conformance testing.
Part two: Model-checking. The issue of modelling a program is considered. The temporal logic CTL is introduced as a formalism to express program properties. CTL model-checking algorithms are presented.
Part three: Abstract interpretation. The underlying theory is introduced and applications in the area of static code analysis are presented. Basic knowledge in logic and theoretical foundations of computer science
Prüfungsleistung: Oral exam over 30 minutes
Lehr- und Lernmethoden: Lecture with beamer and white-board presentation; exercises for the application of theoretical concepts and self-assessment

Empfohlene Literatur
Glenford J. Myers: Methodisches Testen von Programmen. R. Oldenbourg Verlag, 7. Auflage 2001 (Englische Originalfassung: The Art of Software Testing. John Wiley and Sons, 1979)
Gerard J. Holzmann: Design and Validation of Communication Protocols. Prentice Hall Software Series, 1991.
Edmund C. Clarke, Orna Grumberg und Doron A. Peled: Model Checking. MIT Press, 2000.
Flemming Nielson, Hanne Riis Nielson und Chris Hankin: Principles of Program Analysis. Springer Verlag, 1999.

Zusätzliche Informationen
Erwartete Teilnehmerzahl: 25

Zugeordnete Lehrveranstaltungen
UE: Exercise: Introduction to Formal Software Analysis (080045)
Dozent/in: Prof. Dr. Dirk Nowotka
Zeit und Ort: Di 8:30 - 10:00, CAP4 - R.13.1304 a
UnivIS ist ein Produkt der Config eG, Röttenbach
FB4
Dynamik des Ozeanbodens
Forschungsbereiche
Kernthemen
Integrierende Forschungs-Foci
Programme und Projekte
Sonstiges