NWI-IBC024
Software Verification
Course infoSchedule
Course moduleNWI-IBC024
Credits (ECTS)3
CategoryBA (Bachelor)
Language of instructionEnglish
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
Lecturer(s)
Lecturer
B. Garhewal
Other course modules lecturer
Examiner
prof. dr. F.W. Vaandrager
Other course modules lecturer
Lecturer
prof. dr. F.W. Vaandrager
Other course modules lecturer
Coordinator
prof. dr. F.W. Vaandrager
Other course modules lecturer
Contactperson for the course
prof. dr. F.W. Vaandrager
Other course modules lecturer
Academic year2021
Period
KW3  (31/01/2022 to 10/04/2022)
Starting block
KW3
Course mode
full-time
Remarks-
Registration using OSIRISYes
Course open to students from other facultiesYes
Pre-registrationNo
Waiting listNo
Placement procedure-
Aims

Content
This course discusses some of the main ideas, techniques, and results in software verification.  Three techniques that are widely used in practice will be discussed:
  • Model checking, which provides efficient techniques for the exhaustive exploration of state-based models of programs and reactive systems.
  • Static techniques for program analysis.
  • Testing, which provides the counterpart to exhaustive techniques by defining dynamic analyses to detect programming mistakes and correct them.

The course includes weekly assignments that test understanding of the theoretical concepts that have been presented during the lecture, as well as the application of verification tools to illustrative examples.

Instructional Modes
Level

Presumed foreknowledge
This course builds on several of the previous courses in the Computer Science Bachelor's curriculum: A basic knowledge is required of programming (course Imperative Programming, Object Orientation, and Functional Programming), logic (course Beweren & Bewijzen), automata theory (Talen & Automaten), concurrency and synchronization problems, and model checking (course on Operating Systems). Also some of the concepts from the course Semantics & Correctness will be used during Software Verification course (it is fine, however, if you follow these two courses in parallel).
Test information
  • Grading will be based on the exam (70%) and two practical assignments (2x15%).
  • To be admitted to the exam, you should have submitted serious attempts for five out of the seven weekly assignments (there will be five theoretical and two practical assignments). 
  • For the Re-exam the same rules apply. However, there will be no second chance for the weekly assignments.
Specifics

Required materials
Handouts
The course material consists of hand-outs and lecture slides. These will be made available electronically via Brightspace.

Instructional modes
Course
Attendance MandatoryYes

Tests
Exam
Test weight7
Test typeExam
OpportunitiesBlock KW3, Block KW4

Assignments
Test weight3
Test typeAssignment
OpportunitiesBlock KW3