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

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?