Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » FMSoft WS16/17 (Ü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_ws16 [01.03.2017 14:07] (aktuell) – angelegt volschaf | ||
---|---|---|---|
Zeile 1: | Zeile 1: | ||
+ | ==== FMSoft WS16/17 ==== | ||
+ | Pruefer: Tadeusz Litak\\ | ||
+ | Beisitzer: Christopher Rauch | ||
+ | * What are the syntax of LTL and CTL? | ||
+ | * We have E and A in CTL. How is it in LTL? | ||
+ | * So, is CTL more expressive than LTL? | ||
+ | * Give some examples of formulas expressible only in LTL and only in CTL? | ||
+ | |||
+ | * How does model checking in CTL work? | ||
+ | * Can we check fairness constraints with this algorithm? | ||
+ | * When checking for fairness, do we have to check for E< | ||
+ | * Which fixpoint theorem did we use? | ||
+ | |||
+ | * Can you give the partial correctness Hoare rule for WHILE? | ||
+ | * How do we have to extend it for total correctness? | ||
+ | * What is more suited for total correctness than Hoare rules? | ||
+ | * Can you give the definition of wp(WHILE, | ||
+ | |||
+ | * Now to separation logic: Does (A*T)ΛB <-> (A*(A-*B)) always hold? | ||
+ | * Can you give small axioms for our dynamic programming constructs? | ||
+ | * Which rule did we use to derive the global rules? | ||
+ | * Can you give a total axiom and its derivation? | ||
+ | |||
+ | |||
+ | |