Computer System Modeling and Verification

Year:
1st year
Semester:
S2
Onsite in:
CNAM, UBB
Remote:
ECTS range:
6-7 ECTS

Professors

img
Tristan Crolard
CNAM
img
Simona Motogna
UBB
img
Pierre Courtieu
CNAM

Prerequisites:

Computer Science or Computer/Electrical Engineering Bachelor.

Pedagogical objectives:

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.

Evaluation modalities:

continuous reporting, final exam

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

Required teaching material

Teaching volume:
lessons:
28-35 heurs
Exercices:
0-5 hours
Supervised lab:
0-28 hours
Project:

Devices:

  • Laboratory-Based Course Structure
  • Open-Source Software Requirements