Universität Karlsruhe · Institut für Theoretische Informatik · Prof. Dr. P. H. Schmitt · Mattias Ulbrich

Übungsaufgaben zu den Formalen Systemen

Übungsblätter

	Ausgabe am	Abgabe bis	Zusatzmaterial
Übungsblatt 1	25.10.07	2.11.07
Übungsblatt 2	31.10.07	8.11.07
Übungsblatt 3	8.11.07	15.11.07
Übungsblatt 4	15.11.07	22.11.07
Übungsblatt 5	22.11.07	29.11.07
Übungsblatt 6	29.11.07	6.12.07
Übungsblatt 7	6.12.07	13.12.07	KeY Quelle zu Aufgabe 6a / Lösung / Tips
Übungsblatt 8	13.12.07	20.12.07
Übungsblatt 9	20.12.07	10.1.08	(offizielle) OMG OCL 2.0 Spezifikation
Übungsblatt 10	10.1.08	17.1.08	Informationen zur EBNF
Übungsblatt 11	17.1.08	24.1.08
Übungsblatt 12	24.1.08	7.2.08	Zwei Wochen Bearbeitungszeit

Aufgaben anhand formaler Softwarewerkzeuge

	Ausgabe am	Abgabe bis	Abgabe	Zusatzmaterial
Praxisblatt MiniSat	8.11.07	29.11.07	Webinterface	Vergleichende Auswertung
Praxisblatt KeY	6.12.07	10.1.08	Webinterface	Einführung in KeY
Praxisblatt SPIN	24.1.07	12.2.08	Webinterface	Einführung in SPIN / Promela Kurzreferenz / Peterson Quelltexte

Für das Praxisblatt MiniSat gibt es 20 Punkte. Auch für eine nicht korrekte Lösung kann es dabei anteilig Punkte geben.

Für das Praxisblatt KeY gibt es 20 Punkte. Auch für unvollständige Beweise können anteilig Punkte erhalten werden.

Für das Praxisblatt SPIN gibt es 20 Punkte. Auch für unvollständig bearbeitete Teile können anteilig Punkte erhalten werden.

Alte Klausuren

• Sommersemester 2008 II (ohne Musterlösung)
• Sommersemester 2008
• Wintersemester 2007/2008 (ohne Musterlösung)
• Sommersemester 2007 (ohne Musterlösung)
• Wintersemester 2006/2007 (ohne Musterlösung)
• Sommersemester 2006
• Wintersemester 2005/2006 (ohne Musterlösung)

Formale Werkzeuge

Einige Aufgaben auf den diesjährigen Übungsblättern sollen mit Hilfe von Softwarewerkzeugen gelöst werden, die formale Methoden einsetzen. Die Werkzeuge im einzelnen sind:

1. Der SAT-Solver minisat
2. Der Prozess-Model-Checker SPIN
3. Das Softwareverifikationstool/Automatische Beweiser KeY

Sie sind im Studentenpool der ATIS installiert. Jede/r Student/in der Informatik kann sich dort ein Konto einrichten lassen.

Auf die Programme kann unter Linux zugegriffen werden, sobald der Befehl

auf der Kommandozeile eingeben wurde. Wenn Sie wollen, dass die Kommandos dauerhaft verfügbar sind, empfiehlt es sich, diesen Befehl in die Dabei ~/.bashrc bzw. ~/.cshrc in Ihrem Home-Verzeichnis aufzunehmen.