Sie befinden sich hier: Termine » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » FMSoft WS16/17   (Übersicht)

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?