Formal Methods in Software Development

Utbildningsfakta

Kod: DIT272

<p>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 first-order logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software.</p> <p>On the model checking side, we cover the following topics:</p> <p style="margin-left:40px">- a specification language for concurrent processes,<br /> - verifying assertions,<br /> - synchronization,<br /> - verifying safety and liveness properties in temporal logic.</p> <p>On the deductive verification side, we cover the following topics:</p> <p style="margin-left:40px">- a unit level specification language for Java programs,<br /> - a logic for verification of Java programs,<br /> - verification of Java programs, in the sense that the implementation of a unit fulfils the specification.</p>

Behörighet

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 their knowledge of English: English 6/English B from Swedish Upper Secondary School or the equivalent level of an internationally recognized test, for example TOEFL, IELTS.  

Utbildningstillfällen

Varje tillfälle har egna datum och villkor. Avslutade tillfällen behålls som historik och innebär inte att en ny ansökan är öppen.

• Formal Methods in Software Development

  University of Gothenburg

  Startdatum: 2 september 2024

  Slutdatum: 3 november 2024

  Studietakt: 50 %