Module: Software Verification
|Software Verification||Lecture||2||Winter Semester|
|Software Verification||Recitation Section (small)||2||Winter Semester|
Prof. Sibylle Schupp
Recommended Previous Knowledge:
- Automata theory and formal languages
- Computational logic
- Object-oriented programming, algorithms, and data structures
- Functional programming or procedural programming
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.
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.
Students discuss relevant topics in class. They defend their solutions orally. They communicate in English.
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:
Workload in Hours:
Independent Study Time: 124, Study Time in Lecture: 56
Course: Software Verification
- Syntax and semantics of logic-based systems
- Deductive verification
- Proof obligations
- Program properties
- Automated vs. interactive theorem proving
- Model checking
- Property languages
- Tool support
- Timed automata
- Recent developments of verification techniques and applications
- 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