Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » FMSoft WS14/15 (Übersicht)
no way to compare when less than two revisions
Unterschiede
Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.
— | pruefungen:hauptstudium:ls8:fmsoft_ws14 [14.04.2015 09:24] (aktuell) – angelegt ouler | ||
---|---|---|---|
Zeile 1: | Zeile 1: | ||
+ | ==== FMSoft WS14/15 ==== | ||
+ | * Was ist ein Hoare-Triple und wofuer ist es gut? | ||
+ | * Welche Sprache haben wir in der Vorlesung betrachtet? | ||
+ | * Wie ist die Syntax und Semantik davon? | ||
+ | * Welche Probleme gab es bei der Definition der Semantik und wie haben wir sie geloest? (Fixpunktsatz von Kleene) | ||
+ | * Wie sind die Beweisregeln fuer das Hoare-Kalkuel? | ||
+ | * Was ist Korrektheit und was ist Vollstaendigkeit? | ||
+ | * Und dann haben wir also Korrektheit und Vollstaendigkeit von dem Beweiskalkuel gezeigt, oder? (Antwort: Nein! Nur relative Vollstaendigkeit) | ||
+ | * Warum nur relative Vollstaendigkeit und was war das wichtige Werkzeug dabei? | ||
+ | * Wofuer braucht man Boogie? Wie uebersetzt man IMP zu Boogie? | ||
+ | * Was ist das Frameproblem und wie loest man es? | ||
+ | |||
+ | |||
+ | * Wie ist die Syntax und die Semantik von LTL? | ||
+ | * Erklaeren Sie grob das Model-Checking fuer LTL? | ||
+ | * Was ist ein NBA? Was ist der Unterschied zum GNBA? | ||
+ | * Wie uebersetzt man einen GNBA in einen NBA? | ||
+ | * Wie uebersetzt man eine Formel in einen GNBA? | ||
+ | * Wie konstruiert man den Automaten fuer M x A_{\neg \phi}? | ||
+ | * Wie prueft man jetzt, ob die Formel im Modell erfuellt ist? | ||
+ | |||
+ | |