<?xml version="1.0" encoding="UTF-8"?><lom xmlns="http://ltsc.ieee.org/xsd/LOM" xmlns:lomfr="http://www.lom-fr.fr/xsd/LOMFR" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://ltsc.ieee.org/xsd/LOM http://www.lom-fr.fr/xsd/lomfrv1.0/std/lomfr.xsd">
<general>
<identifier>
<catalog>Canal-U_Ocms</catalog>
<entry>8737</entry>
</identifier>
<title><string language="fre"><![CDATA[Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème partie]]></string></title>
<language>FRE</language>
<description>
<string language="fre"><![CDATA[Nous présentons les systèmes embarqués critiques et les exigences
qui leur sont liées : dans certains cas (nucléaire, avionique,
santé) aucun bug n'est accepté. Puis nous présentons l'analyse
statique, que nous illustrons sur un exemple de programme. Nous
montrons que pour analyser des variables numériques (entiers et
réels) il faut utiliser des notions géométriques telles que les
intervalles et les polygones. Nous montrons ensuite que
l'analyse des boucles (boucles while et boucles for) requiert
des techniques d'accélération. Nous terminons avec des exercices
réalisés avec l'outil concurinterproc qui permet d'analyser
un programme et de démontrer des propriétés essentielles pour
garantir l'absence de bug.]]></string></description>
<keyword><string language="fre"><![CDATA[algorithmique]]></string></keyword><keyword><string language="fre"><![CDATA[treillis de Galois]]></string></keyword><keyword><string language="fre"><![CDATA[preuve de programme]]></string></keyword><keyword><string language="fre"><![CDATA[analyse de programme]]></string></keyword><keyword><string language="fre"><![CDATA[sémantique programmation]]></string></keyword><keyword><string language="fre"><![CDATA[génie logiciel]]></string></keyword>
<lomfr:documentType>
<lomfr:source>LOMFRv1.0</lomfr:source>
<lomfr:value>image en mouvement</lomfr:value>
</lomfr:documentType>
</general><lifeCycle>
<contribute>
<role>
<source>LOMv1.0</source>
<value>content provider</value>
</role>
<entity><![CDATA[BEGIN:VCARD
VERSION:3.0
CLASS:PUBLIC
REV:2021-09-16 17:44:40
FN:INRIA (Institut national de recherche en informatique et automatique)
N:INRIA (Institut national de recherche en informatique et automatique);;;;
URL;TYPE=work:http://www.inria.fr/
ROLE:content provider
TZ:+0200
END:VCARD
]]></entity>
<date><dateTime>2012-01-18</dateTime></date>
</contribute>
<contribute>
<role>
<source>LOMv1.0</source>
<value>content provider</value>
</role>
<entity><![CDATA[BEGIN:VCARD
VERSION:3.0
CLASS:PUBLIC
REV:2021-09-16 17:44:40
FN:Académie de Grenoble
N:Académie de Grenoble;;;;
URL;TYPE=work:Académie de Grenoble
ROLE:content provider
TZ:+0200
END:VCARD
]]></entity>
<date><dateTime>2012-01-18</dateTime></date>
</contribute>
<contribute>
<role>
<source>LOMv1.0</source>
<value>content provider</value>
</role>
<entity><![CDATA[BEGIN:VCARD
VERSION:3.0
CLASS:PUBLIC
REV:2021-09-16 17:44:40
FN:MANHATTAN STUDIO PRODUCTIONS M.S.P.
N:MANHATTAN STUDIO PRODUCTIONS M.S.P.;;;;
URL;TYPE=work:Manhattan Studio Productions 
ROLE:content provider
TZ:+0200
END:VCARD
]]></entity>
<date><dateTime>2012-01-18</dateTime></date>
</contribute>
<contribute>
<role>
<source>LOMv1.0</source>
<value>author</value>
</role>
<entity><![CDATA[BEGIN:VCARD
VERSION:3.0
CLASS:PUBLIC
REV:2021-09-16 17:44:40
FN:Alain GIRAULT
N:GIRAULT;Alain;;;
URL;TYPE=work:http://pop-art.inrialpes.fr/people/girault/
ROLE:author
NOTE:Alain Girault est chercheur à Inria Grenoble - Rhône-Alpes, après avoir fait son doctorat au laboratoire Verimag et fait un an de postdoc à Inria, à Nice puis un an à l'Université de Berkeley (USA). Il est spécialiste en méthodes formelles pour la conception de systèmes embarqués. 
TZ:+0200
END:VCARD
]]></entity>
<date><dateTime>2012-01-18</dateTime></date>
</contribute>
<contribute>
<role>
<source>LOMv1.0</source>
<value>author</value>
</role>
<entity><![CDATA[BEGIN:VCARD
VERSION:3.0
CLASS:PUBLIC
REV:2021-09-16 17:44:40
FN:Bertrand JEANNET
N:JEANNET;Bertrand;;;
URL;TYPE=work:http://pop-art.inrialpes.fr/~bjeannet/
ROLE:author
NOTE:Bertrand Jeannet est chercheur à Inria Grenoble - Rhône-Alpes, après avoir fait son doctorat au laboratoire Verimag et passé 4 ans à Inria, à Rennes. Il est spécialiste dans l'analyse statique de programmes par des méthodes d'interprétation abstraite. 
TZ:+0200
END:VCARD
]]></entity>
<date><dateTime>2012-01-18</dateTime></date>
</contribute>
</lifeCycle>
<metaMetadata>
<metadataSchema>LOMv1.0</metadataSchema>
<metadataSchema>LOMFRv1.0</metadataSchema>
</metaMetadata>
<technical>
<format>video/mp4</format>
<location><![CDATA[https://www.canal-u.tv/video/inria/analyse_de_programmes_a_quoi_ca_sert_comment_ca_marche_2eme_partie.8737]]></location>
<location><![CDATA[https://streaming-canal-u.fmsh.fr/vod/media/canalu/videos/fuscia/analyse.de.programmes.a.quoi.a.sert.comment.a.marche.2.me.partie_8737/jeannet.02.2.mp4]]></location>
<location><![CDATA[https://streaming-canal-u.fmsh.fr/vod/media/canalu/videos/fuscia/analyse.de.programmes.a.quoi.a.sert.comment.a.marche.2.me.partie_8737/jeannet.02.2.mp4]]></location>
<size>225272549</size>
<duration><duration>PT0H57M20S</duration></duration>
</technical>
<educational>
<learningResourceType>
<source>LOMv1.0</source>
<value>lecture</value>
</learningResourceType>
<context>
<source>LOMv1.0</source>
<value>formation continue</value>
</context>
</educational>
<rights>
<cost>
<source>LOMv1.0</source>
<value>no</value>
</cost>
<copyrightAndOtherRestrictions>
<source>LOMv1.0</source>
<value>no</value>
</copyrightAndOtherRestrictions>
<description>
<string language="fre"><![CDATA[Droits réservés à l'éditeur et aux auteurs. 
Document libre, dans le cadre de la licence Creative Commons (http://creativecommons.org/licenses/by-nd/2.0/fr/), citation de l'auteur obligatoire et interdiction de désassembler (paternité, pas de modification)]]></string>
</description>
</rights>
<relation>
<kind>
<source>LOMv1.0</source>
<value>ispartof</value>
</kind>
<resource>
<identifier>
<catalog>URI</catalog>
<entry>https://www.canal-u.tv/producteurs/inria/science_info_lycee_profs_conferences_de_formation_des_professeurs_du_secondaire_en_science_informatique</entry>
</identifier>
<description>
<string language="fre"><![CDATA[Science Info Lycée Profs : conférences de formation des professeurs du secondaire en science informatique.]]></string>
</description>
</resource>
</relation>
<classification>
<purpose>
<source>LOMv1.0</source>
<value>discipline</value>
</purpose>
<taxonPath>
<source>
<string language="fre"><![CDATA[Universités Numériques Thématiques 2009 http://www.universites-numeriques.fr]]></string>
</source>
<taxon>
<id/>
<entry>
<string language="fre"/>
</entry>
</taxon>
</taxonPath>
</classification>
<classification>
<purpose>
<source>LOMv1.0</source>
<value>discipline</value>
</purpose>
<taxonPath>
<source>
<string language="fre">CDD 22e éd.</string>
<string language="eng">DDC 22nd ed.</string>
</source>
<taxon>
<id>005.3</id>
<entry>
<string language="fre"><![CDATA[Programs]]></string>
</entry>
</taxon>
</taxonPath>
</classification> </lom>