Contactez-nous
  • Génie logiciel

Computer Systems Modeling and Verification

Mis à jour le

Responsable(s) : M. Stefano SECCI

  • Cours + travaux pratiques
Code Cnam : USEEN1

Envie d'en savoir plus sur cette formation ?

Afin d’obtenir les tarifs, le calendrier de la formation, en distanciel, en présentiel, le lieu de la formation et un contact, remplissez les critères suivants :

Afficher le centre adapté à mes besoins

Afin d’obtenir les tarifs, le calendrier de la formation et le lieu de la formation, remplissez les critères suivants :

  • Durée : 50 heures
  • Package
  • 6 crédits

Présentation

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

Prérequis

Computer Science or Computer/Electrical Engineering Bachelor.

Objectifs

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.

Compétences et débouchés

Parcours

Programme

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és d'évaluation

Lab reports and written final exam.

Ces formations pourraient vous intéresser