Module Description

Module: Software Verification

Courses:

TitleTypeHrs/WeekPeriod
Software VerificationLecture2Winter Semester
Software VerificationRecitation Section (small)2Winter Semester

Module Responsibility:

Prof. Sibylle Schupp

Admission Requirements:

None

Recommended Previous Knowledge:

  • Automata theory and formal languages
  • Computational logic
  • Object-oriented programming, algorithms, and data structures
  • Functional programming or procedural programming
  • Concurrency

Educational Objectives:

Professional Competence

Theoretical Knowledge

Students apply the major verification techniques in model checking and deductive verification. They explain in formal terms syntax and semantics of the underlying logics, and assess the expressivity of different logics as well as their limitations. They classify formal properties of software systems. They find flaws in formal arguments, arising from modeling artifacts or underspecification. 

Capabilities

Students formulate provable properties of a software system in a formal language. They develop logic-based models that properly abstract from the software under verification and, where necessary, adapt model or property. They construct proofs and property checks by hand or using tools for model checking or deductive verification, and reflect on the scope of the results. Presented with a verification problem in natural language, they select the appropriate verification technique and justify their choice.   

Personal Competence

Social Competence

Students discuss relevant topics in class. They defend their solutions orally. They communicate in English. 

Autonomy

Using accompanying on-line material for self study, students can assess their level of knowledge continuously and adjust it appropriately.  Working on exercise problems, they receive additional feedback. Within limits, they can set their own learning goals. Upon successful completion, students can identify and precisely formulate new problems in academic or applied research in the field of software verification. Within this field, they can conduct independent studies to acquire the necessary competencies and compile their findings in academic reports. They can devise plans to arrive at new solutions or assess existing ones. 

ECTS-Credit Points Module:

6 ECTS

Examination:

Written exam

Workload in Hours:

Independent Study Time: 124, Study Time in Lecture: 56


Course: Software Verification

Language:

English

Period:

Winter Semester

Content:

  • Syntax and semantics of logic-based systems
  • Deductive verification
    • Specification
    • Proof obligations
    • Program properties
    • Automated vs. interactive theorem proving
  • Model checking
    • Foundations
    • Property languages
    • Tool support
  • Timed automata
  • Recent developments of verification techniques and applications

Literature:

  • C. Baier and J-P. Katoen, Principles of Model Checking, MIT Press 2007.
  • M. Huth and M. Bryan, Logic in Computer Science. Modelling and Reasoning about Systems, 2nd Edition, 2004.
  • Selected Research Papers