Agenda

Coopération entre modèles de temps et de communication

La modélisation et la simulation : de la physique aux langages et aux logiciels

L'électricité est constructive : l'équivalence entre la propagation électrique et le calcul Booléen constructif pour les circuits synchrones cycliques

Langages pour la programmation des systèmes hybrides temps discret/temps continu

Jouer avec le temps

Programmation de systèmes parallèles temps-réel : défis et réussites des approches synchrones et par réseaux de Kahn

Cerveau, cognition et temps

Le temps dans le calcul neuronal

Discussion et réponses aux questions de l'année

La révolution informatique dans les sciences

De la spécification à la réalisation, au test et à la preuve : les approches formelles

L'Internet des objets, une révolution à ne pas manquer

Les méthodes générales : assertions, réécriture, interprétation abstraite, logiques et assistants de preuve

Utilisation des méthodes formelles pour la sécurisation de systèmes complexes : une avancée industrielle

Des logiques d'ordre supérieur à la programmation vérifiée en Coq

Langages et systèmes pour la preuve interactive

La vérification de modèles (model-checking)

Prouver la sécurité informatique : la logique à la rescousse

Vérification et optimisation booléennes d'automates et circuits

Spécification, construction et vérification de programmes : le parcours d'une pensée scientifique sur une quarantaine d'années

L'importance des langages en informatique

Intégration de la vérification formelle dans les langages de programmation (INRIA de Rennes)

Les BDDs (Binary Decision Diagrams) et leurs applications

Application des BDDs dans la conception de circuits intégrés

SAT : la satisfaction booléenne

SAT : des victoires contre les problèmes difficiles

SMT : la satisfaction modulo théories

SMT en pratique : le démonstrateur Alt-Ergo

La vérification formelle de programmes temporisés