Difference between revisions of "TU Wien:Programm- und Systemverifikation VU (diverse)"

From VoWi
Jump to navigation Jump to search
m (Ergänzungen zu UE, Ablauf etc)
m (Sprache ergänzt)
 
(One intermediate revision by the same user not shown)
Line 10: Line 10:
 
     {{Zuordnung|E033534|Programm- und Systemverifikation|wahl=1}}
 
     {{Zuordnung|E033534|Programm- und Systemverifikation|wahl=1}}
 
     {{Zuordnung|E033535|Programm- und Systemverifikation}}
 
     {{Zuordnung|E033535|Programm- und Systemverifikation}}
}}
+
|sprache=en}}
 
{{mattermost-channel|programm-und-systemverifikation}}
 
{{mattermost-channel|programm-und-systemverifikation}}
  
Line 24: Line 24:
  
 
== Ablauf ==
 
== Ablauf ==
ss20: zweimal wöchentlich 2h Vorlesung, UE Blätter ausgegeben im März, April, Mai, jeweils ca 2 Wochen Zeit.
+
ss20: <s>zweimal wöchentlich 2h Vorlesung</s> 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
 
Vorlesung bis Ende Mai

Latest revision as of 12:49, 26 March 2020

Daten[edit]

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

Inhalt[edit]

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

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

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.

Vortrag[edit]

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.

Übungen[edit]

  • 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

Prüfung, Benotung[edit]

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 Zeugnisausstellung[edit]

SS18: Test 19.06.2019; Ergebnisse: 29.06.2019;

Zeitaufwand[edit]

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.

Unterlagen[edit]

noch offen

Tipps[edit]

noch offen

Verbesserungsvorschläge / Kritik[edit]

noch offen