Computer Systems Modeling and Verification
Public Concerné
Computer Science or Computer/Electrical Engineering Bachelor.
Objectifs pédagogiques
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.
Contenu de la formation
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
- 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
Description des modalités de validation
Attendance and participation in lessons (50%) and written final exam (50%).
Prévisions d'ouverture
| Groupe | Semestre | Modalité | État d'ouverture | Date du premier cours | Lieux | ||
|---|---|---|---|---|---|---|---|
| USEEN1 | Computer Systems Modeling and Verification | 6 | Cours de Jour | - | - | - | - |
Voir les dates et horaires, les lieux d'enseignement et les modes d'inscription sur les sites internet des centres régionaux qui proposent cette formation
