Description

Most of the course is devoted to high-level semantic design and code-level properties. The emphasis is put on executable specifications and verification tools based on the following methods:

• Static analysis and type checking
• Design-by-contract and property-based testing

Static and dynamic verification in particular are compared in this course, with a focus on tools and prototype development:

• Preliminaries
  • Imperative programming and unit testing
  • Functional programming and logic
• Part I: static analysis
  • Specification: typing rules (deductive system)
  • Implementation: mode-based extraction of functional code
• Part II: dynamic verification
  • Specification: design-by-contract
  • Implementation: self-testing and property-based testing

Finalité

Students who take this course will gain an understanding of the concepts and theories of computer-aided formal specification and verification, and learn how to use and write formal verification tools.

Description des modalités d'évaluation

Lab reports and written final exam.

Prérequis

Computer Science or Computer/Electrical Engineering Bachelor.