Techniques de vérification et de validation

  • Enseignant: Michael Blondin
  • Plan de cours: 
  • Horaire:
    – mardi: 13h30 à 15h20 au D3-2029
    – mercredi: 15h30 à 16h20 au D3-2029
  • Examen final: mercredi 24 avril de 09h00 à 12h00 au local D3-2029
  • Disponibilité sans rendez-vous: jeudi de 14h30 à 15h30
  • Rétroaction de mi-session

Calendrier

Matériel

Références

Outils

  • Solveurs logiques: Z3 (démo en ligne), Z3, CVC4
  • LoLA peut être téléchargé à partir d'ici  . Système modélisé en classe:  
  • NuSMV peut être téléchargé à partir d'ici  . Systèmes modélisés en classe:  
  • Spin peut être téléchargé à partir d'ici  . L'interface graphique utilisée en classe est iSpin; elle également disponible sur ce site Web. Il existe une autre interface nommée jSpin. Vous pouvez alternativement utiliser l'interface Web  développée à Chalmers University of Technology.

Introduction

Devoirs

Contact

  • michael.blondinusherbrooke.ca
  • Bureau D4-1024-1 (Pavillon D4, 1er étage)
    Sur rendez-vous ou le jeudi de 14h30 à 15h30