Master Course
Program Verification

WebHome
- Education Page
- Description
- Literature
- Schedule
- Assignments

Center
Master Program

Center

Page

Web

Wiki

Log In or Register

Education Page

Pv

Program verification

Website:website containing additional information
Course code:INFOPV
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!
formgrouptimeweekroomteacher
college   ma 13-1517-20,22,24-26 BBL-420 Wishnu Prasetya
  
wo 11-1317,18,20,22-26 BBL-420
practicum   di 11-1317-20,22-26 BBL-453
wo 13-1517,18,20,22-26 BBL-453
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.
wijzigen?

The page above is included from http://www.cs.uu.nl/education/vak.php?vak=pv&jaar=2003