Modulcode:	Inf-GSoZu
Englische Bezeichnung:	Introduction to Formal Software Analysis
Modulverantwortliche(r):	Prof. Dr. Dirk Nowotka
Turnus:	unregelmäßig (WS11/12 SS13 WS14/15 SS16 SS18 SS19 WS21/22 SS24)
Präsenzzeiten:	4V 2Ü
ECTS:	8
Workload:	60 Std. Vorlesung, 30 Std. Präsenzübung, 150 Std. Selbststudium
Dauer:	ein Semester
Modulkategorien:	BSc-Inf-WP (BSc Inf (21)) WI (BSc Inf (15)) WISSE (BSc Inf) MSc-Inf-WP (MSc Inf (21)) 2F-MEd-Inf-WP (MEd-Hdl Inf (21)) 2F-MA-Inf-WP (2F-MA Inf (21)) WI (MSc Inf (15)) WI (MSc WInf (15)) WI (MEd Inf) WPI (MEd Inf)
Lehrsprache:	Englisch
Voraussetzungen:	Inf-LogInf Inf-TGI

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.

Weitere Voraussetzungen:

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

Verwendbarkeit:

Master "Computer Science"

Literatur:

Glenford J. Myers: 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.

Verweise:

Kommentar: