Differences

This shows you the differences between two versions of the page.

--- official:goals [2012/05/24 11:37]
paddy [Sheet 6]
+++ official:goals [2012/07/06 18:05]
paddy
@@ Line 80: / Line 80: @@
   * First case study about specifying models, properties and proving their consistency.
+===== Sheet 7 =====
+  * Two more complex case studies for specifying models, properties and proving their consistency.
+  * Be able to define advanced models.
+  * Be able to specify properties for such models.
+  * Be able to prove those properties with regard to the models.
+  * Understand and proof properties on paper about lattices and fixpoints.
+  * Be able to specify inductive sets on paper and understand their semantics.
+===== Sheet 8 =====
+  * Get familiar with LTL.
+  * Be able to specify properties about transition systems in LTL.
+  * Be able to do proofs of LTL properties, using the semantics.
+  * Get to know one possible definition of traces and transition systems and how to use it for proofs.
+  * First steps in defining a calculus for an embedded logic in Isabelle/HOL and using the calculus to do proofs.
+  * Learn how the specification affects proofs and how changes in the specification can help the proofs.
+===== Sheet 9 =====
+  * Understand the difference between different styles of semantics.
+  * Be able to prove properties about language semantics.
+  * Be able to do induction over inductive sets / predicates.

Isabelle/HOL Support Wiki