|Website:||website containing additional information|
|Credits:||7.5 ECTS (=5.25 old credit points)|
|Period:||periode 4 (week 17 t/m 27, dwz 19-4-2004 t/m 2-7-2004; herkansing week 35)
|Participants:||up till now 7 subscriptions|
|Schedule:||Dit is een oud rooster!
|Contents:||Thanks to computers, our modern society is able to multiply its productivity to a revolutionary level. The other side of this is that we have also become overly dependant on them that the risk of errors with costly consequences have increased to the point that actually can no longer be ignored. The traditional testing approach has become inadequate. In the past two decades, people have invested a lot in an alternative approach called program verification. It is based on the formal method and is far more superior to testing because of its complete coverage. It is a very active research area, and right now people are working hard to try to make the approach to scale up.
In this course you will be exposed to state of the art program verification techniques. A lot of attention will be given to the use of tools, since it is almost impossible to verify real programs without ones. In particular, we will show you two techniques: theorem proving and model checking. They are complementary: one is a general approach, and the other is specialized. In addition, we will also show you the primary internals of a verification tool, so you know the basics needed to write your own verification tool.
|Literature:||Lecture notes. |
|Course form:||Lectures + programming training.|
|Exam form:||Assignments + either final assignments or an exam (depending on the number of participants).
There will be two sets of assignments: HOL and Spin, each consists of 3 assignments. Your assignment cummulative will be 0.66 of your HOL average + 0.34 of your SPIN average.
Your end grade will be the average of your exam (or final assignment) and your assignment cummulative.|
|Minimum effort to qualify for 2nd chance exam:||Om aan de aanvullende toets te mogen meedoen is ontbreken van ten hoogte 1 toetsactiviteit toegestaan.|