TU Wien:Programm- und Systemverifikation VU (diverse)

DatenEdit

Lecturers Prof. Georg Weissenbacher
ECTS 6
Department Informationssysteme
When summer semester
Language English
Abbreviation PSV
Links tiss:184741 , Mattermost-Channel
Zuordnungen
Bachelor Software & Information Engineering Wahlmodul Programm- und Systemverifikation
Bachelor Technische Informatik Pflichtmodul Programm- und Systemverifikation

Mattermost: Channel "programm-und-systemverifikation"RegisterMattermost-Infos

InhaltEdit

Zitat von helmi77 (Informatik-Forum):

Der Themenkreis ist im Grunde sehr interessant, es geht unter anderem um

  • Aussagenlogik (SAT Solver): wie lässt sich effizient feststellen ob eine gegebene Formel erfüllbar ist
  • Assertions: wozu benötigt man Assertions, was erreicht man durch die Verwendung (cf. Hoare Logik)
  • Testabdeckung: wie kann man feststellen, ob ein Programm ausreichend getestet wurde
  • Temporal Logic: logische Aussagen in zeitlicher Hinsicht
  • Hoare Logic: Aussagen über die Korrektheit eines Programmes

AblaufEdit

ss20: zweimal wöchentlich 2h Vorlesung wegen COVID-19 nur Aufzeichnungen von ss19, UE Blätter ausgegeben im März, April, Mai, jeweils ca 2 Wochen Zeit.

Vorlesung bis Ende Mai

Prüfung Mitte Juni.

Benötigte/Empfehlenswerte VorkenntnisseEdit

Kenntnis der Programmiersprache C bzw. C++ von Vorteil, da sich in den Slides immer wieder Fragmente von C Programmen finden. Bei der ersten Übung war im SS 2014 gefordert ein vorgegebenes C Programm um Assertions zu erweitern, mit dem Ziel etwaige Bugs zu finden.

ss 20: keine, es wird alles ausführlich erklärt. Technisches Englisch ist aber von Vorteil.

S21: Gleich wie S20. Keine Vorkenntnisse nötig. Es hilft aber sicher wenn man vorher TIL gehört hat. Aber grundsätzlich wird in der VO alles wiederholt und eingeführt was man braucht.

VortragEdit

Der Vortrag wird durchwegs auf Englisch abgehalten, die Einheiten von Prof. Weissenbacher sind in der Regel sehr interessant gestaltet, seine Aussprache ist überraschend gut, alles in allem Wert zuzuhören.

Die Vorträge werden aufgezeichnet. Leider schreibt der Vortragende immer wieder etwas an die Tafel zwischendurch, und das sieht man dann in der Vorlesungsaufzeichnung nicht. Es kann daher schwierig sein dem Vortrag zu folgen, wenn man die Aufzeichnungen nur online ansieht.

Im S21 wurde die VO ausschließlich von Prof. Weissenbacher gehalten. Ich fand den Vortrag sehr gut. Tempo und Inhalt haben immer gepasst. Es wird viel mit Beispielen gearbeitet.

ÜbungenEdit

  • 90 Punkte in 6 assignments

15p - assertions & inductive invariant
25p - equivalence/boundary value testing & coverage criteria
10p - propositional logic / SAT
15p - SMT in Z3
15p - Temporal Logic and Model Checking
10p - Hoare Logic

  • ca. 2 Woche Zeit für assignment
  • benotung von assignments war OK. Leider kein Feedback.

SS16:

  • 80 Punkte in 6 Übungsblätter
    • Assertions, Testing, Coverage: 20p
    • Satisfiability: 10p
    • SMT Solvers: 10p
    • Temporal Logic: 10p
    • Model Checking: 10p
    • Hoare Logic and Bounded Model Checking: 20p

SS20:

50% der Note setzten sich aus 3 Übungsblättern zusammen

  • Assertions, Testing, Coverage: 20p
  • Hoare Logic and Bounded Model Checking: 20p
  • Temporal Logic and Automated Reasoning: 20p

Prüfung, BenotungEdit

SS14:

  • Sowohl in der Pruefung als auch in den Uebungen koennen Sie 90 Punkte erreichen (insgesamt also 180). Um positiv bewertet zu werden, muessen Sie insgesamt zumindest die Haelfte der Punkte erreichen. Der Notenschluessel wird voraussichtlich wie folgt aussehen (halbe Punkte werden aufgerundet):

(< 90: 5) (90-112: 4) (113-135: 3) (136-157: 2) (158-180: 1)

SS16: Bei den Übungen und bei den Prüfungen kann man jeweils 80 Punkte sammeln, was insgesamt 160 Punkte ergibt. Für eine positive Note benötigt man insgesamt (Übungsteil + Prüfungsteil) mindestens 81 Punkte. Es wird nur ein schriftlicher Termin angeboten. Für diejenigen, die bei dem Termin nicht dabei sein können, gibt es die Möglichkeit eine mündliche Prüfung zu machen. Falls sich viele Leute für die mündliche Prüfung melden, wird eine zweite schriftliche Prüfung angeboten.

Man hat nur einen Test- bzw. Prüfungsantritt. Geht man zum Test und reichen die Punkte vom Test + Übungen insgesamt nicht für eine positive Note, so bekommt man jedenfalls ein negatives Zeugnis ausgestellt. Wenn man die LVA wiederholt, muss man den Übungsteil nicht noch einmal machen, sondern kann die Übungspunkte vom vorherigen Antritt übernehmen.

Dauer der ZeugnisausstellungEdit

SS18: Test 19.06.2019; Ergebnisse: 29.06.2019;

ZeitaufwandEdit

SS14: Keine Vorlesung besucht. ca. 1-2 Tage (6-12 St.) für Assignment. Für Prüfung ca. 10 Stunden alle Assignments durchgegangen.

SS20: alle VOs (online) besucht.

UnterlagenEdit

noch offen

TippsEdit

So viel wie möglich bei den Übungen machen. Bekommt man dort alle Punkte, benötigt man bei der Prüfung nur noch einen einzigen Punkt für eine positive Note

Wenn irgendwo Verständnisprobleme sind, im TUWEL Forum nachfragen. Der Professor antwortete normalerweise sehr schnell und ausführlich, oft auch mit weiteren Beispielen

Die Prüfungen sind vom Aufbau her immer relativ gleich. Die Beispiele ändern sich, aber die Struktur war in den letzten Jahren unverändert.

Die Übungsaufgaben stammen meist von den Prüfungen der letzten Semester.

Verbesserungsvorschläge / KritikEdit

Ich fand die LVA angenehm und lehrreich. Die 6 ECTS sind hier auch sehr großzügig bemessen (Ich habe ca. 40h gebraucht, was eher 2 ECTS entspricht). Kollegen hatten ähnlich wenig Aufwand.