Portail nationalFormation

Computer Systems Modeling and Verification

Code UE : USEEN1

  • Cours + travaux pratiques
  • 6 crédits

Responsable(s)

Tristan CROLARD

Public, conditions d’accès et prérequis

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.

Mots-clés

Contenu

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

Modalité d'évaluation

Attendance and participation in lessons (50%) and written final exam (50%).

Cette UE apparaît dans les diplômes et certificats suivants

Chargement du résultat...
Patientez

Contact



Voir le site

Voir le calendrier, le tarif, les conditions d'accessibilité et les modalités d'inscription dans le(s) centre(s) d'enseignement qui propose(nt) cette formation.

Enseignement non encore programmé