Document - Université catholique de Louvain
Contents
1. Universit Catholique de Louvain DESCRIPTIF DE COURS 2015 2016 LSINF2224 UCL Universit Programming methods catholique de Louvain 5 0 cr dits ECTS 30 0 h 15 0 h Enseignants Pecheur Charles Langue Anglais d enseignement Lieu du cours Louvain la Neuve Ressources en ligne gt http icampus uclouvain be claroline course index php cid LINF2224 Th mes abord s Fondements de la programmation leurs propri t s s mantique validit et preuve Analyse d ductives de programme logique de Hoare pr conditions les plus faibles conditions de v rification invariants et variants Automatisation de preuves boucles proc dures et r cursion structures de donn es programme r actif M thodes d analyse comportementales machine d tats logique temporelle model checking abstraction Acquis Eu gard au r f rentiel AA du programme Master ing nieur civil en informatique ce cours contribue au d veloppement l acquisition et l valuation des acquis d apprentissage suivants d apprentissage INFO1 1 3 INFO2 5 INFOS 3 INFO5 5 INFO6 1 INFO6 3 Eu gard au r f rentiel AA du programme Master 120 en sciences informatiques ce cours contribue au d veloppement l acquisition et l valuation des acquis d apprentissage suivants SINF1 M3 SINF2 5 SINF5 3 SINF5 5 SINF6 1 SINF6 3 Les tudiants ayant suivi avec fruit ce cours seront capables de d f2. es cours magistraux des s ances de travaux pratiques mod lisation et analyse de programmes et des missions o les tudiants utilisent un logiciel de v rification automatique ESC Java Java PathFinder afin de prouver des propri t s de programmes Java Via leurs nonc s des missions sont clairement balis es Le r sultats attendus la m thodologie utiliser les outils exploiter y sont pr sent s Le code du programme analyser est anot et l nonc comporte un bref manuel d utilisation L outil de preuve de programme ou de model checking qui doivent tre utilis s sont clairement indiqu s Pour faciliter leur prise en main par les tudiants des s ances d exercices sont pr vues De plus une consultance est assur e par les encadrants du cours en cas de probl me Chaque mission fait l object d un bref rapport crit qui servira de base pour l valuation D monstration Introduction Fondements Programmes s quentiels Conditions de v rification Proc dures R cursion Structures de donn es Programmes r actifs Mod les bas s sur des tats Model Checking Abstraction Support de cours ransparents en ligne Bibliographie B Liskov J Guttag Program Development in Java Abstraction Specification and Object Oriented Design Addison Wesley 2001 O J Dahl Verifiable Programming Prentice Hall 1992 K R Apt E R Olderog Verification of Sequential and Concurrent Program
3. inir et formaliser les principes de l analyse et la v rification de introduit dans les cours de baccalaur at d crire et appliquer les techniques qui permettent ces principes d tre automatis s sur un ordinateur illustrer le potentiel et les limites de ces techniques par des exemples concrets Les tudiants auront d velopp des comp tences m thodologiques et op rationnelles En particulier ils ont d velopp leur capacit formaliser sous forme math matique un probl me donn r diger un rapport technique bref reprend les principaux l ments d un travail d analyse argumenter l oral La contribution de cette UE au d veloppement et la ma trise des comp tences et acquis du des programme s est accessible la fin de cette fiche dans la partie Programmes formations proposant cette unit d enseignement UE UCL LSINF2224 page 1 3 Modes d valuation des acquis des tudiants M thodes d enseignement Contenu Bibliographie Autres infos Facult ou entit en charge Universit Catholique de Louvain DESCRIPTIF DE COURS 2015 2016 LSINF2224 3 missions 45 de la note finale Th orie examen oral 55 de la note finale Une liste de questions est fournie la fin du quadrimestre Les missions devront tre pr sent es au cours du quadrimestre de cours Elles ne pourront pas tre repr sent es lors des sessions d examens ult rieures Le cours combine d
4. s Springer Verlag 1991 Loeckx K Sieber The Foundations of Program Verification 2nd Ed Wiley Teubner 1984 D Gries The Science of Computer Programming Springer Verlag 1981 Pr alables LINGI1122 UCL LSINF2224 page 2 3 Universit Catholique de Louvain DESCRIPTIF DE COURS 2015 2016 LSINF2224 Programmes formations proposant cette unit d enseignement UE Master 120 en sciences f SINF2M 5 informatiques Master 120 ing nieur civil en INFO2M 5 informatique Master 120 bioing nieur nn Bi BIRC2M 5 chimie et bioindustries Master 120 bioing nieur sciences et technologies de BIRE2M 5 l environnement Master 120 bioing nieur gestion des for ts et des BIRF2M 5 espaces naturels Master 120 bioing nieur BIRA2M 5 sciences agronomiques UCL LSINF2224 page 3 3
Download Pdf Manuals
Related Search