Description
Introduction aux méthodes formelles en génie logiciel avec couverture de la logique propositionnelle et du premier ordre (syntaxe, sémantique, théorie de la démonstration), langages de spécification formelle, analyse bornée et validation, outils de spécification formelle, et model checking avec machines à états finis, logique temporelle et outils de model checking.
Préalables
- Prérequis : COMP 1805 , SYSC 3120 , et SYSC 4001 .
Conditions et modalités
- Prérequis : COMP 1805 , SYSC 3120 , et SYSC 4001 .
- Cours magistral de trois heures par semaine.
Texte de référence dans sa langue d’origine
Introduction to formal methods in software engineering with coverage of propositional and first-order logic (syntax, semantics, proof theory), formal specification languages, bounded analysis and validation, formal specification tools, and model checking with finite-state machines, temporal logic, and model checking tools.
- Prerequisite(s): COMP 1805 , SYSC 3120 , and SYSC 4001 .
- Lectures three hours a week.
Sources et références
Les dates et les sources sont conservées pour vous aider à vérifier les renseignements. Les traductions sont proposées pour faciliter la lecture; la source officielle fait référence pour les conditions et les exigences.
Référence source : https://calendar.carleton.ca/undergrad/courses/SYSC/