==== 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 ECXφ, ECφUΨ and ECGφ?
* 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?