Le workshop CAFEIN vise à réunir des experts des méthodes formelles, des systèmes hybrides, ainsi que des partenaires industriels et des fournisseurs d'outils pour élaborer, développer et valider de nouvelles techniques de coopérations de méthodes formelles dans le but d'augmenter le degré d'automatisation et donc d'applicabilité de la vérification formelle. Plus particulièrement, nous voulons appliquer ces nouvelles techniques sur des modèles haut niveau, tout en nous intéressant à la compilation de ces modèles vers du code embarqué.
Ce workshop fait suite au projet ANR du même nom qui avait pour objectif d'étudier et développer des la outils pour la vérification formelle de propriétés fonctionnelles sur des spécifications haut niveau de systèmes critiques, en particulier des systèmes de contrôle-commande décrits en Lustre qui interagissent avec un environnement physique. La complexité de ces systèmes a connu une croissance exceptionnelle ces dernières années, croissance motivée par des avancées techniques mais aussi par des motivations économiques et environnementales. De plus, ces systèmes sont soumis à de fortes contraintes liées à la certification. Devant cette hausse de complexité, le processus de certification, à base de tests essentiellement, a montré ses limites, et les méthodes formelles apparaissent comme une alternative crédible. La norme DO-178C intègre cette évolution en recommandant l'usage de méthode formelles et de techniques basées sur les modèles pour le processus de développement, vérification et de validation des systèmes critiques. Cependant, malgré un intérêt croissant des utilisateurs industriels, la vérification formelle n'est pas encore prête pour un déploiement conséquent dans les processus de développement. Pour les applications industrielles, une intervention humaine, coûteuse en temps de développement et en main d'oeuvre, est encore nécessaire pour obtenir des résultats précis.
Voici une liste non exhaustive des thèmes de recherche en lien avec le workshop CAFEIN:
Analyse statique par interprétation abstraite
Synthèse de code
Vérification de systèmes hybrides
Model Checking
Preuves automatiques de propriétés numériques
Langages de programmation, techniques de compilation
Démonstration automatique
LIEU
Le workshop CAFEIN aura lieu à Hôtel Llaret aux Angles.
Appel à contributions
La date limite pour s’inscrire et soumettre une proposition d’exposé est fixée au 31 janvier 2023.
Pour l'inscription, requise que vous proposiez un exposé ou non, utilisez le lien "Mon inscription" disponible dans le menu de gauche de ce site.
Pour assurer le bon déroulement de l’événement, nous vous prions de vous inscrire et de soumettre une éventuelle proposition d’exposé en respectant les dates limites détaillées plus loin.
Nous vous invitons à ne pas attendre la date limite et à vous inscrire dès que possible, même si vous ne proposez pas d’exposé.
Frais d'inscriptions
Les frais d'inscription au workshop CAFEIN, fixes pour chaque participant, sont 550€. Cela inclut :
Les frais d'hébergment en chambre simple ou double pour 2 nuits.
Tous les repas à partir du mercredi midi jusqu'au vendredi midi.
Les pauses cafés entre les sessions d'exposés.
Nous proposons également un forfait à 700€ incluant la nuit du mardi et le repas du soir.
Pour s'inscrire au workshop, merci d'envoyer un email à Sylvain.Conchon@universite-paris-saclay.fr. Les instructions pour le paiement vous seront alors communiquées.
Chargement... 
