Christoph Schwarzweller: Teaching





Seminarium w semestrze letnim 2005: Programowanie generyczne


Wykład w semestrze letnim 2005: Semantyka programów


Seminarium w semstrze zimowym 2004/2005: Programowanie generyczne


Wykład w semestrze zimowym 2004/2005: Metody formalnej specyfikacji


Laboratorium w semestrze letnim 2004: Zaawansowane języki programowania


Laboratorium w semestrze letnim 2004: Języki programowania I


Laboratorium w semestrze zimowym 2003/2004: Wstwp do Prologu


Laboratorium w semestrze zimowym 2003/2004: Wstęp do programowania


Vorlesung im SS 03: Arithmetische Algorithmen


Zeit und Ort:
Vorlesung: Di. 17:00-19:00 Uhr, Do. 17:00-19:00 Uhr, MS N2
Übung: n.V.
Umfang: 4 + 2; -> 4ff
Prüfungsfach:
Theoretische/Praktische Informatik

Beschreibung:
Hauptziel der Vorlesung ist eine sorgfältige Untersuchung der vier arithmetischen Grundoperationen: Addition, Subtraktion, Multiplikation und Division. Viele betrachten Arithmetik als eine triviale Sache, die Kinder lernen und Rechner abarbeiten, doch wir werden sehen, dass Arithmetik ein faszinierender Gegenstand mit vielen interessanten Facetten ist. Es ist wichtig, effiziente Methoden für das Rechnen mit Zahlen zu studieren, da Arithmetik so vielen Rechneranwendungen zu Grunde liegt.
Arithmetik ist in der Tat eine lebendige Sache, die in der Weltgeschichte eine bedeutende Rolle spielte und die sich immer noch in schneller Entwicklung befindet. In der Vorlesung werden wir Algorithmen vorstellen an vielen Arten von Größen wie ganz großen Zahlen, Brüchen (rationalen Zahlen) und Polynomen; und wir werden auch damit zusammenhängende Themen wie Basiswechsel, Faktorisierung von Zahlen und die Auswertung von Polynomen, sowie Anwendungen in der Kryptographie (RSA-Algorithmus) besprechen.




Praktikum im WS 02/03: Einführung in das Mizar-System


Zeit und Ort: n.V., Sand R225
Umfang: 0 + 4; -> 5ff
Prüfungsfach:
Theoretische/Praktische Informatik

Beschreibung:
Das Mizar System ist ein Beweisüberprüfer (proof checker), d.h. das System überprüft automatisch in einer speziellen Sprache formulierte Beweisskripte. Die Mizar Sprache stellt sowohl Konstrukte zur Definition von Objekten und deren Eigenschaften, als auch Konstrukte zum Führen von Beweisen zur Verfügung. Daher kann Mizar auch als ein Sytem zur Unterstützung von Spezifikation und Verifiaktion angesehen werden.
In diesem Praktikum sollen der Umgang mit dem Mizar System erlernt und einfache Beweisaufgaben aus verschiedenen Bereichen (z.B. rationale Zahlen, kommutative Algebra) gelöst werden.




Vorlesung im SS 02: Arithmetische Algorithmen


Zeit und Ort:
Vorlesung: Di. 18:10-19:55 Uhr, Do. 17:10-18:55 Uhr, MS N2
Übung: n.V.
Umfang: 4 + 2; -> 4ff
Prüfungsfach:
Theoretische/Praktische Informatik

Beschreibung:
Hauptziel der Vorlesung ist eine sorgfältige Untersuchung der vier arithmetischen Grundoperationen: Addition, Subtraktion, Multiplikation und Division. Viele betrachten Arithmetik als eine triviale Sache, die Kinder lernen und Rechner abarbeiten, doch wir werden sehen, dass Arithmetik ein faszinierender Gegenstand mit vielen interessanten Facetten ist. Es ist wichtig, effiziente Methoden für das Rechnen mit Zahlen zu studieren, da Arithmetik so vielen Rechneranwendungen zu Grunde liegt.
Arithmetik ist in der Tat eine lebendige Sache, die in der Weltgeschichte eine bedeutende Rolle spielte und die sich immer noch in schneller Entwicklung befindet. In der Vorlesung werden wir Algorithmen vorstellen an vielen Arten von Größen wie ganz großen Zahlen, Brüchen (rationalen Zahlen) und Polynomen; und wir werden auch damit zusammenhängende Themen wie Basiswechsel, Faktorisierung von Zahlen und die Auswertung von Polynomen, sowie Anwendungen in der Kryptographie (RSA-Algorithmus) besprechen.




Vorlesung im WS 01/02: Formale Spezifikationsmethoden


Zeit und Ort:
Vorlesung: Mi. 12 Uhr, Sand 6/7, KS
Übung: n.V., Sand, (14-tägig)
Umfang: 2 + 1; -> 5ff
Prüfungsfach:
Theoretische/Praktische Informatik

Beschreibung:
Das Ziel einer Spezifikation ist die möglichst genaue Beschreibung des Verhaltens eines Systems, an der sich eine Implementierung orientieren kann. Dabei sind formale Methoden wünschenswert, da diese ein hohes Maß an Präzision und Zuverlässigkeit ermöglichen.
In der Vorlesung wird zunächst eine Einführung in die algebraische Spezifikation gegeben. Anschließend wird auf modellbasierte Spezifikationsmethoden eingegangen.




Vorlesung im SS 01: Arithmetische Algorithmen


Zeit und Ort:
Vorlesung: Di. 15-17 Uhr, Do. 17-19 Uhr, MS N2
Übung: n.V.
Umfang: 4 + 2; -> 4ff
Prüfungsfach:
Theoretische/Praktische Informatik

Beschreibung:
Hauptziel der Vorlesung ist eine sorgfältige Untersuchung der vier arithmetischen Grundoperationen: Addition, Subtraktion, Multiplikation und Division. Viele betrachten Arithmetik als eine triviale Sache, die Kinder lernen und Rechner abarbeiten, doch wir werden sehen, dass Arithmetik ein faszinierender Gegenstand mit vielen interessanten Facetten ist. Es ist wichtig, effiziente Methoden für das Rechnen mit Zahlen zu studieren, da Arithmetik so vielen Rechneranwendungen zu Grunde liegt.
Arithmetik ist in der Tat eine lebendige Sache, die in der Weltgeschichte eine bedeutende Rolle spielte und die sich immer noch in schneller Entwicklung befindet. In der Vorlesung werden wir Algorithmen vorstellen an vielen Arten von Größen wie ganz großen Zahlen, Brüchen (rationalen Zahlen) und Polynomen; und wir werden auch damit zusammenhängende Themen wie Basiswechsel, Faktorisierung von Zahlen und die Auswertung von Polynomen, sowie Anwendungen in der Kryptographie (RSA-Algorithmus) besprechen.




Seminar im WS 00/01: Gröbnerbasen


Zeit und Ort: n.V., Sand R225
Umfang: 0 + 2; -> 5ff
Prüfungsfach:
Theoretische/Praktische Informatik

Beschreibung:
Gröbnerbasen erlauben die algorithmische Behandlung einer Reihe von Fragen über Polynomringe und deren Ideale. 1965 von Buchberger eingeführt, finden Gröbnerbasen mittlerweile immer häufiger Anwendung in der Computeralgebra, insbesondere beim Lösen von Polynomgleichungen sowie beim geometrischen Beweisen.
In den Vorträgen sollen zunächst die Grundlagen der Gröbnerbasen-Theorie behandelt und der Buchberger-Algorithmus zu deren Berechnung vorgestellt werden. Anschließend wird auf verschiedene Erweiterungen und Anwendungen von Gröbnerbasen eingegangen.




Praktikum im SS 00: Mechanisches Beweisen


Zeit und Ort: n.V., Sand R225
Umfang: 0 + 4; -> 6ff
Prüfungsfach:
Theoretische/Praktische Informatik

Beschreibung:
Das Mizar System ist ein Beweisüberprüfer (proof checker), d.h. das System überprüft automatisch in einer speziellen Sprache formulierte Beweisskripte. Die Mizar Sprache stellt sowohl Konstrukte zur Definition von Objekten und deren Eigenschaften, als auch Konstrukte zum Führen von Beweisen zur Verfügung. Daher kann Mizar auch als ein Sytem zur Unterstützung von Spezifikation und Verifiaktion angesehen werden.
In diesem Praktikum sollen der Umgang mit dem Mizar System erlernt und einfache Beweisaufgaben aus verschiedenen Bereichen (z.B. rationale Zahlen, kommutative Algebra, Listen) gelöst werden.




Vorlesung im WS 99/00: Spezifikation und Verifikation II


Zeit und Ort:
Vorlesung: Mi. 14 Uhr, Sand R225
Übung: n.V., Sand, R225 (14-tägig)
Umfang: 2 + 1; -> 5ff
Prüfungsfach:
Theoretische Informatik

Beschreibung:
Spezifikation und Verifikation sind eng miteinander verbunden: Eine exakte Spezifikation ist Voraussetzung für eine formale Verifikation. Diese besteht nun darin, nachzuweisen, daß ein gegebener Algorithmus eine gegebene Spezifikation erfüllt. Dabei ist natürlich maschinelle Unterstützung sowohl bei der Spezifikation als auch bei der Verifikation wünschenswert.
Die Vorlesung behandelt die grundlegenden Methoden zur Verifikation von Programmen. Dazu werden verschiedene Semantiken von Programmiersprachen (operationelle, axiomatische und denotationelle Semantik) eingeführt und die daraus resultierenden Verifikationsverfahren besprochen.




Vorlesung im SS 99: Spezifikation und Verifikation


Zeit und Ort:
Vorlesung: Mo, 14 Uhr, Sand, R225
Übung: n.V., Sand R225
Umfang: 2 + 1; -> 5ff
Prüfungsfach:
Theoretische Informatik

Beschreibung:
Spezifikation und Verifikation sind eng miteinander verbunden: Eine exakte Spezifikation ist Voraussetzung für eine formale Verifikation. Diese besteht nun darin, nachzuweisen, daß ein gegebener Algorithmus eine gegebene Spezifikation erfüllt. Dabei ist natürlich maschinelle Unterstützung sowohl bei der Spezifikation als auch bei der Verifikation wünschenswert.
In dieser Vorlesung werden die Grundlagen der algebraischen Spezifikation besprochen. Zentrale Punkte sind dabei loose und initiale Semantik, Erweiterung und Modularisierung von Spezifikationen und parametrisierte Spezifikationen. Anschließend wird auf dieser Basis die Begriffsbeschreibungssprache Tecton vorgestellt.



back to
Zakład Informatyki