Les méthodes formelles appliquées au lo-
giciel ont fait des progrès importants lors des deux
dernières décennies. Leur application à l'embarqué est
ainsi un succès indéniable. Parmi les prochains défis
réside la question de leur application à des domaines
moins contraints. Par exemple, le développement en C
de logiciels non-critiques utilise régulièrement l'inser-
tion d'assembleur « en ligne », que ce soit pour optimi-
ser certaines opérations ou pour accéder à des primi-
tives systèmes autrement inaccessibles. Ceci empêche
complètement l'utilisation des méthodes développés
pour le C pur. Nous proposons ici TInA, une méthode
générale, automatique, sûre et orientée vérification
pour pouvoir porter le code assembleur en ligne vers
un code C sémantiquement équivalent, et profiter en
retour des analyses pré-existantes pour ce langage. Nos
expérimentations sur du code C d'envergure montrent
la faisabilité et l'intérêt de l'approche.