Spezialvorlesung: Computer-Supported Modeling and Reasoning

Organizer:	Prof. Dr. David Basin and Dr. Burkhart Wolff and Dr. Jan-Georg Smaus (exercises)
Classes:	Wed 9-11 in Building 101, 01-018
Exercises:	Fri 9-11 in Building 52, 00-005
Credit points:	6
Exam:	Students who actively participate in the course and exercises will get a "benoteten Schein".
Language:	English
Prerequisites:	The lecture is intended both for students of Artificial Intelligence (KI) interested in computer-supported deduction-based problem solving, and students interested in computer based system modeling and program verification. Some basic knowledge of logic will be of great use for successful participation in this lecture.

This Spezialvorlesung (2+2) aims at teaching new ways of thinking about program development and program analysis, as well as providing practical experience in formal computer-supported verification.

The lecture consists of two parts. In part 1, we shall introduce the foundations of logic reasoning and their implementation in the modern proof system Isabelle. The accompanying practical exercises will be from the fields of logic, (naïve) set theory and discrete mathematics.

In part 2 we shall study the consistent construction of mathematical theories on a large scale, the representation (embedding) of programming languages in logic and verification of programs or program refinements.

Comments? Send an email to J.-G. Smaus.