Computer System Modeling and Verification
Year:
1st year
Semester:
S2
Programme main editor:
I2CAT
Onsite in:
CNAM, UBB
Remote:
ECTS range:
6-7 ECTS
Professors
Tristan Crolard
CNAM
Simona Motogna
UBB
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