Computer Systems Modeling and Verification

Code UE : USEEN1

  • Cours + travaux pratiques
  • 6 crédits



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.

Compétences visées

  • Write formal specifications and contracts
  • Understand how source code and specs are represented in logic
  • Verify functional properties of programs with automated tools
  • Perform simulations of models and verifications of properties


Most of the course is devoted to high-level semantic design and code-level properties. The emphasis is put on tool-based specification and validation methods, used in safety-critical applications industry, and based on the following formal methods:
  • Static analysis and symbolic execution
  • Bounded model-checking and k-induction
  • Deductive verification and semi-automated theorem provers
Two formal methods in particular are compared in this course.

Method I: Code-level Specification (language: Ada)
  • Based on the design by contract paradigm for Ada
  • Formal semantics, same syntax as host programming langage
  • Executable specifications embedded in source code
  • Verification tools integrated with the default IDE
Method II: Model-based Development (language: Lustre)
  • Executable specification language for synchronous reactive systems
  • Designed for efficient compilation and formal verification
  • Automatic analysis with tools based on model-checking techniques

Modalité d'évaluation

Homework assignments and written final exam.


  • Jean-Francois Monin : Understanding Formal Methods
  • John W. McCormick, Peter C. Chapin : Building High Integrity Applications with SPARK
  • Nicolas Halbwachs : Synchronous Programming of Reactive Systems

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

Chargement du résultat...
Intitulé de la formation
Lieu(x) Package
Lieu(x) Paris
Intitulé de la formation Type Modalité(s) Lieu(x)


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 programmé s'il s'agit d'un diplôme, d'un certificat ou d'une UE ou enseignement qui ne fait jamais l'objet d'une programmation s'il s'agit d'une UA ou d'une US (le code formation commence alors par UA ou US).