IGSE CSC 7204
Master of Science
The purpose of formal methods is to enable the construction of large, highly reliable software. Formal Methods is a generic term for system design, analysis, implementation and verification methods that are described and used with mathematical rigor.
In particular formal specification techniques allow for the construction of automated verification tools that can perform tests on specifications and corresponding code to find errors in implementations (and also in requirements and models)
The course will focus on verification by testing and by proving.
A standard background on programming and logics (helpful but not required)
software engineering – formal methods – design by contract – specification - verification – proof – structural testing – conformance testing -
Introduction to software engineering and formal methods
Propositional and first order logics (syntax, semantics, deduction) – Notion of contract – Axiomatic specification – Hoare logics – Verification of functional properties Introduction to model based verification and design
Structural testing: path predicates – coverage – generation of test cases -oracles - Model based testing - Conformance testing
Project or exam