TU Wien:Programm- und Systemverifikation VU (diverse)

Aus VoWi
Wechseln zu: Navigation, Suche

Daten[Bearbeiten]

Inhalt[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]

noch offen

Benötigte/Empfehlenswerte Vorkenntnisse[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.

Vortrag[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. Den Einheiten von Prof. Veith zu folgen ist, aufgrund seiner Aussprache, zeitweise schwierig. SS16: Da Prof. Veith leider von uns gegangen ist, hat der Prof. Weissenbacher seinen Teil übernommen.

Übungen[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


Prüfung, Benotung[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.

Dauer der Zeugnisausstellung[Bearbeiten]

SS18: Test 19.06.2019; Ergebnisse: 29.06.2019;

Zeitaufwand[Bearbeiten]

noch offen

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

Unterlagen[Bearbeiten]

noch offen

Tipps[Bearbeiten]

noch offen

Verbesserungsvorschläge / Kritik[Bearbeiten]

noch offen