1. Overview

In this chapter, we provide an outline of the course, along with a brief motivation and key learning outcomes.

1.1. Motivation

As embedded and distributed systems are becoming ever more ubiquitous, we depend increasingly on the correctness of the software that controls such systems. This course studies the formal specification, verification, and synthesis of software.

1.2. Key learning outcomes

  • An understanding of the role of formal methods in the construction of software systems

  • Proficiency in the representative methods and tools, such as

    • design-by-contract

    • property-based testing

    • model-checking sequential and concurrent systems

1.3. Course outline

To be expanded…

  • software engineering context

  • logic foundations

  • design by contract

  • property-based testing

  • modeling and model checking

    • sequential systems

    • concurrent systems

  • run-time verification

1.4. Bloom’s taxonomy

The letters refer to the successive levels of learning from the cognitive domain of Bloom’s taxonomy:

  • K: know/remember the term

  • C: comprehend/understand the concept

  • A: apply the technique

  • analyze/evaluate/create (advanced levels)

Todo

map Bloom levels to course outline