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<sub>C</sub>Xφ, E<sub>C</sub>φUΨ and E<sub>C</sub>Gφ?
 +  * 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,B)?
 +
 +  * 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?
 +
 +
 +