La XXIX° édition des journées FAC a eu lieu les 3 et 4 avril 2024 au LAAS-CNRS. Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’ENAC, l’INSA Toulouse, ISAE-Supaero, l’ONERA, Toulouse-INP et de l’Université Toulouse III, Paul Sabatier. Programme des journées Mercredi 3 avril 09h00 : accueil et présentation des journées 09h30-10h30 : Invited talk. Laurent Mounier (Vérimag, Univ. Grenoble): Vérification formelle pour la détection et l’analyse de vulnérabilités logicielles

La XXVIII° édition des journées FAC a eu lieu les 5 et 6 avril 2023 à l’ISAE. Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’INSA Toulouse, de l’ISAE, de l’ONERA et de l’Université Toulouse III, Paul Sabatier. Programme des journées Mercredi 5 avril 09h00 : accueil présentation des journées 09h30-10h30 : Invited talk. Mathieu Martel : (LAMPS, Univ. Perpignan) Matrix Computations: In Seek of Frugality

La XXVII° édition des journées FAC a eu lieu les 14 et 15 octobre 2021 à l’ENAC (bâtiment Bréguet, amphithéâtre Bellonte, 7, avenue Édouard-Belin, Toulouse). Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’INSA Toulouse, de l’ISAE et de l’ENAC. Programme des journées Jeudi 14 octobre 09h00 : accueil présentation des journées

La XXVII° édition des journées FAC devait avoir lieu en avril 2020 à l’ISAE. Pour raison de crise sanitaire qu’il n’est pas necessaire de préciser, la réunion a dû être annulée. Nous souhaitions néanmoins garder une trace des exposés qui avaient été programmé et remercier chaleureusement nos collègues qui avaient proposé une présentation, ainsi que nos conférenciers invités, Cezara Drăgoi (INRIA & ENS Paris) et Jean-Christophe Filliatre (LRI, Université Paris Sud & CNRS / INRIA Saclay).

La XXVI° édition des journées FAC a eu lieu les 27 et 28 mars prochain à l’IRT Saint Exupéry (bâtiment B612, Toulouse). Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’INSA Toulouse. Programme des journées: Mercredi 27 mars 09h00 : accueil présentation des journées et actualités du chantier IFSE par Marc Pantel 09h30-10h30 : Karine Heydemann, (LIP6 / Univ. Pierre et Marie Curie): Attaques en faute: modélisation, sécurisation et analyse de robustesse de code.

La XXV° édition des journées FAC a eu lieu les 4 et 5 avril 2018 à l’IRIT - site UPS. Ces journées sont organisées par le groupe IFSE du RTRA STAE. Programme des journées Mercredi 4 avril 09h00 : accueil - présentation des journées et actualités du chantier IFSE par Marc Pantel 09h30-10h30 : Katell Morin-Allory, (TIMA / Univ. Grenoble Alpes) : Assertions et systèmes matériels. 10h30-11h00 : pause 11h00-12h00 : Automatic Conformance Testing of Safety Instrumented Systems for Offshore Oil Platforms. Veiga H.W., de Queiroz M.H., Farines JM., de Lima M.L

Ces journées sont organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2017 se sont tenues les 29 et 30 mars à l’ONERA. Programme des journées : Mercredi 30 mars 09h00 : accueil 09h30-10h30 : Catherine Dubois, ENSIIE : Interopérabilité des prouveurs : Dedukti, Zenon et FoCaLize à la rescousse. 10h30-11h00 : pause 11h00-12h00 : systèmes distribués Asynchronous Communication Models: a Menagerie of Refinements. Florent Chevrou, Aurélie Hurault, Shin Nakajima, Philippe Quéinnec

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2016 ont eu lieu les 30 et 31 mars au LAAS. Programme des journées : Mercredi 30 mars 9h00 : accueil 9h30-10h30 : Yliès Falcone, Univ. Grenoble I — LIG : On the Runtime Enforcement of (Timed) Properties. 10h30-11h00 : pause 11h00-12h30 : sûreté de fonctionnement et politiques d’informations Développement automatique d’applications tolérantes aux fautes. K. Delmas, R. Delmas, C. Pagetti

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2015 ont eu lieu les 22 et 23 avril 2015 à IRIT - SITE ENSEEIHT (SALLE DES THÈSES, C002). Programme des journées : Mercredi 22 avril 9h00 : accueil 9h30-10h30 : Ahmed Bouajjani Paris 7, LIAFA : Verification of Concurrent Programs: Decidability, Complexity, Reductions. abstract: Concurrency is omnipresent in computer systems, at all levels, from applications relying on high level synchronization mechanisms and using abstract data structures, to low level code implementing concurrent/distributed data structures and system services over multi-core architectures/large-scale networks. The automated verification of concurrent programs is a challenging problem due to their highly complex behaviours. We will address the problem of verifying automatically concurrent programs, from the point of view of decidability and complexity. We will show the difficulties that raise in addressing this problem in different contexts: shared-memory, message passing, dynamic creation of tasks, recursion, relaxed memory models, etc. We will overview existing approaches for handling these issues, and we will show in particular how verification problems for concurrent programs can be reduced to ”simpler” problems (stated as reachability queries either on sequential programs, or on concurrent but sequentially consistent programs) for which there are already know verification algorithms and tools.

Ces journées ont été organisées par le groupe IFSE du RTRA STAE. Les journées FAC'2014 ont eu lieu les 16 et 17 avril 2014 à l’ONERA, salle du boulon. Programme des journées : Mercredi 16 avril 9h00 : accueil 9h15 : ouverture des journées par W. Wiels, adjointe au directeur du DTIM 9h30-10h30 : John Mullins PolyTech Montréal: Vérification et mesure du flux d’information abstract: Les politiques de sécurité du flux d'information expriment des restrictions sur l'information qui peut être acquise par les utilisateurs d'un système. Dans cet exposé, nous considérerons le problème de la vérification et de la mesure du flux d'information dans un système. La difficulté de ces problèmes réside dans le fait que, contrairement aux propriétés fonctionnelles (qualitatives ou quantitatives) des systèmes qui s'expriment comme ensembles d'exécutions, les propriétés de flux d'information s'expriment comme ensembles d'ensembles d'exécutions. Nous présenterons d'abord un schéma formel appelé opacité qui permet d'exprimer dans le cadre uniforme des systèmes de transitions, le système, l'attaquant et la politique de sécurité. Nous verrons que le problème de vérification de cette politique est décidable pour les systèmes finis, un attaquant à mémoire finie et un secret régulier. Nous verrons également comment le problème de la vérification de la plupart des propriétés de flux d'information se réduit à celui de l'opacité. Nous étendrons ensuite ce schéma au cadre des processus de décision markoviens étiquetés et poserons le problème du calcul de diverses mesures de flux d'information dans un système.