This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
official:goals [2012/06/13 10:23] paddy |
official:goals [2012/06/20 10:54] paddy |
||
---|---|---|---|
Line 89: | Line 89: | ||
* Understand and proof properties on paper about lattices and fixpoints. | * Understand and proof properties on paper about lattices and fixpoints. | ||
* Be able to specify inductive sets on paper and understand their semantics. | * 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. | ||