Formal Methods in Software Development

About this programme

No fees are charged for EU and EEA citizens, Swedish residence permit holders and exchange students. The aim of this course is to teach knowledge and skills in, and judgement about, two important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced in three ways: conceptual, theoretical, and practical, using a particular tool. The course builds on skills in firstorder logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software. - verification of Java programs, in the sense that the implementation of a unit fulfils the specification. Successfully completed courses corresponding to 120 credits within the subject Computer Science or equivalent, specifically DIT201 Logic in Computer Science, 7.5 credits, and a 7.5 credits course in object-oriented programming (or equivalent) are required. Applicants must prove knowledge of English: English 6/English level 2 or the equivalent level of an internationally recognized test, for example TOEFL, IELTS. Selection is based upon the number of credits from previous university studies, maximum 285 credits