CloseHelpPrint
Kies de Nederlandse taal
Course module: 192114300
192114300
Program Verification
Course info
Course module192114300
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact personprof.dr. M. Huisman
E-mailm.huisman@utwente.nl
Lecturer(s)
Contactperson for the course
prof.dr. M. Huisman
Lecturer
prof.dr. M. Huisman
Academic year2016
Starting block
2B
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
Learning goals
After the course, the student will be able to explain the purpose of program verification and to apply it on different programs. Concretely, he or she will be able to:
  • Express the operational semantics of (object-oriented), sequential and multi-threaded programs.
  • Be able to explain the relation and differences between operational, denotational and axiomatic semantics.
  • Formulate the semantics of logics used for formulating properties of such programs, in particular permission-based separation logic.
  • Explain and compare the proof principles behind sequential programming, and in particular reasoning about object invariants.
  • Explain and compare the proof principles behind multi-threaded programming.
  • Evaluate expressions in such logics on the basis of the operational semantics.
  • Formulate and prove useful logic properties of such programs
Content
Program verification is one of the most effective ways to improve the reliability of software. Techniques to guarantee software reliability are essential for many different application domains. They can be used to ensure the correctness of for example safety-critical applications, or electronic purse applications, but also to prevent common program errors, such as uncaught exceptions or nullpointer dereferencing. Rather than relying on the programmer's skill and intuitions only, program verification provides formal arguments and evidence for the correctness of programs. Thus, program verification can be used to prove correctness of a program, in contrast to only proving incorrectness, as testing does. During this course, the student will become acquainted with a selection of methods and tools currently used for the verification of object-oriented and multi-threaded programs. This includes in particular operational semantics and logics for reasoning about such programs, such as design-by-contract logic and separation logic.
 
This course builds on the System Validation course, where program validation is discussed from a user’s perspective. Knowledge attained during the lectures will be applied during the four mandatory exercise sessions and in two homework assignments, one to be done individually, one to be done in pairs. Additionally, the students will also be asked to read and present some recent papers describing different approaches to various aspects of program verification. These presentation sessions will end with a discussion to understand strength and weaknesses of the different approaches. In the assignments students will use and become acquainted with the latest tools, used in actual research. The results of the assignments combined with the grade for the presentations will determine the final grade.
 
Prerequisites• Extensive knowledge of logic and proofs This is offered in the masters course Advanced Logic (192111092)• Extensive knowledge about programspecification techniques, such as JML annotations, which is offered in the course System Validation (192140122)
Assumed previous knowledge
-
PARTICIPATING STUDY
M-CSC
Required materials
Articles
Various papers announced on blackboard.
Recommended materials
-
Instructional modes
Lecture

Project

Tutorial

Tutorial

Tests
Assignment

CloseHelpPrint
Kies de Nederlandse taal