TU Wien:Programm- und Systemverifikation VU (diverse)

Aus VoWi
Zur Navigation springen Zur Suche springen
Ähnlich benannte LVAs (Materialien):

Daten[Bearbeiten | Quelltext bearbeiten]

Vortragende Prof. Georg Weissenbacher
ECTS 6
Alias Program and System Verification (en)
Letzte Abhaltung 2024S
Sprache English
Abkürzung PSV
Mattermost programm-und-systemverifikation • Register • Mattermost-Infos
Links tiss:184741
Zuordnungen
Bachelorstudium Informatik Modul Programm- und Systemverifikation (Breite Wahl)
Bachelorstudium Software & Information Engineering Modul Programm- und Systemverifikation (Gebundenes Wahlfach)
Bachelorstudium Technische Informatik Modul Programm- und Systemverifikation (Pflichtfach)


Inhalt[Bearbeiten | Quelltext bearbeiten]

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

Ablauf[Bearbeiten | Quelltext bearbeiten]

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 Vorkenntnisse[Bearbeiten | Quelltext bearbeiten]

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.

Vortrag[Bearbeiten | Quelltext bearbeiten]

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.

Übungen[Bearbeiten | Quelltext bearbeiten]

  • 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, Benotung[Bearbeiten | Quelltext bearbeiten]

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.

S21: Die Prüfung ähnelte stark den Übungsaufgaben. Ähnliche Beispiele und Komplexität. Es gibt zwar nur einen offiziellen Prüfungstermin, aber der Professor bietet individuell mündliche Prüfungen an die man wahrnehmen kann wenn man die Prüfung verpasst hat (oder evtl. auch wenn man eine negative Note erhalten hat?). Bei der mündlichen Prüfung bekommt man Aufgaben gestellt und etwas Zeit um diese zu bearbeiten. Anschließend bespricht man die Lösung mit dem Professor und bekommt wahrscheinlich noch Theorie fragen dazu gestellt. Zur Benotung lässt sich sagen, dass ich sie recht großzügig fand. Wenn man bei den Übungen alle Punkte bekommen hat, braucht man nur noch einen einzigen Punkt um positiv zu sein. Daher sollte sich eine gute Note locker ausgehen wenn man bei den Übungen brav mitmacht. Bei den Übungen hat der Professor meiner Meinung nach auch sehr großzügig bewertet. Solange man die Übung ernsthaft versucht hat, gab es auch für teilweise falsche Lösungen noch fast alle Punkte.

S23: Ich muss der vorherigen Aussage aus dem S21 wiedersprechen. In unserem Semester wurde sehr streng bei den Übungsaufgaben bewertet. Teilweise hat man auch auf richtige Sachen Minuspunkte bekommen, die wurden wenn man sich bei der Lehrveranstaltung gemeldet hat, teilweise aber auch zurückkorrigiert. Also dass man für falsche Lösungen fast alle Punkte bekommt, kann ich nicht unterschreiben. Meist war es eher so dass man einen kleinen Fehler hatte und dann gleich die Hälfte der Punkte abgezogen worden sind.

Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]

SS18: Test 19.06.2019; Ergebnisse: 29.06.2019; 10 days

SS21: Test 15.06.2021; Ergebnisse:

Zeitaufwand[Bearbeiten | Quelltext bearbeiten]

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

SS21: alle VOs (online) besucht. VOs wurden online abgehalten, je ca 1.5h Vortrag. Für die Aufgabenblätter ca 8-10h pro Arbeitsblatt (alle Bsp gelöst), man könnte sicher aber auch weniger investieren. Anschließend eigentlich nur 1-2 Tage je 4h für die Prüfung geübt. Insgesamt recht wenig aufwand für 6 ECTS (Mein Aufwand waren genau 60h, also eher 2.5 ECTS).

Unterlagen[Bearbeiten | Quelltext bearbeiten]

Folien über TUWEL, Aufzeichnungen der VO auf PeerTube. Kein offzielles Buch oder Skript.

Tipps[Bearbeiten | Quelltext bearbeiten]

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 / Kritik[Bearbeiten | Quelltext bearbeiten]

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.

Abgerufen von „https://vowi.fsinf.at/index.php?title=TU_Wien:Programm-_und_Systemverifikation_VU_(diverse)&oldid=184603“