==== 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?