Liste de toutes les réunions Working Group à venir et passées proposées par l'équipe MDSC

Liste des WG MDSC passées

Jeudi 13 décembre 2018 de 10:30 à 11:30
SAT and Bounded Model Checking from a practitioner perspective
MDSC / C&A

Type : Séminaire
Titre : SAT and Bounded Model Checking from a practitioner perspective
Intervenant(s) :
Valentin Montmirail
Lieu d'exercice : Laboratoire I3S
Date et lieu : Jeudi 13 décembre 2018 de 10:30 à 11:30 , Salle de réunion du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

Within a decade, the use of SAT related technologies moved from a confidential interest among specialists to a popular tool for solving discrete combinatorial problems. Improvements in the practical resolution of SAT is driven by applications: Bounded Model Checking in Electronic Design Automation has been a major component for the success of SAT engines for solving "real" combinatorial problems at the end of the 90s, Bioinformatic and Software engineering are currently two areas where SAT engines receive a lot of interest.
In this talk, we will focus on the theory behind modern SAT solvers tailored to solve "real" combinatorial problems, and discuss their application to the bounded model checking problem. The talk will introduce the generic SAT engine architecture used in all the so-called "CDCL SAT solvers" inherited from the original MiniSAT (www.minisat.se) and see how its development has been driven by the Bounded Model Checking problem.

Vendredi 7 décembre 2018 de 10:30 à 11:30
Towards a constraint system for round-off error analysis of floating-point computation
MDSC

Type : Séminaire
Titre : Towards a constraint system for round-off error analysis of floating-point computation
Intervenant(s) :
Rémy Garcia
Lieu d'exercice : I3S
Date et lieu : Vendredi 7 décembre 2018 de 10:30 à 11:30 , Salle de réunions du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

Computation over floating-point numbers induces errors due to rounding. Those errors are at the root of many problems, such as the precision or the stability of computation. Numerous works, which are based on an overestimation of actual errors, try to address similar issues. However, they do not provide critical information to reason on those errors, for example, by computing input values that exercise a given error.
We introduce a new constraint solver aimed at analysing the round-off errors that occur in floating-point computations. Such a solver allows reasoning on round-off errors by means of constraints on ranges of error values. This new solver is built by incorporating in a solver for constraints over the floating-point numbers the domain of errors which is dual to the domain of values. Both domains, the domain of values and the domain of errors, are associated with each variable of the problem. Additionally, we introduce projection functions that filter these domains as well as the mechanisms required for the analysis of errors.

Vendredi 23 novembre 2018 de 10:30 à 12:30
Introduction à la programmation par contraintes
MDSC / C&A

Type : Séminaire
Titre : Introduction à la programmation par contraintes
Intervenant(s) :
Pelleau Marie
Lieu d'exercice : I3S
Date et lieu : Vendredi 23 novembre 2018 de 10:30 à 12:30 , Salle de réunions du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

La PPC permet de formaliser et résoudre des problèmes fortement combinatoires, dont le temps de calcul évolue en pratique exponentiellement. Les méthodes développées aujourd'hui résolvent efficacement de nombreux problèmes industriels de grande taille dans des solveurs génériques. Cependant, les solveurs restent dédiés à un seul type de variables : réelles ou entières, et résoudre des problèmes mixtes discrets-continus suppose des transformations ad hoc. Dans un autre domaine, l'IntAbs permet de prouver des propriétés sur des programmes, en étudiant une abstraction de leur sémantique concrète, constituée des traces des variables au cours d'une exécution. Plusieurs représentations de ces abstractions, appelées domaines abstraits, ont été proposées. Traitées de façon générique dans les analyseurs, elles peuvent mélanger les types entiers, réels et booléens, ou encore représenter des relations entre variables. En partant du constat qu'en PPC et en IntAbs, des sur-approximations d'un ensemble désiré sont calculées, la notion de domaines abstraits en IntAbs a été redéfinie en PPC afin de construire une méthode de résolution traitant indifféremment les entiers et les réels. Cette généralisation permet d'intégrer à la PPC des domaines relationnels, comme les octogones déjà utilisés en IntAbs. En exploitant l'information spécifique aux octogones pour guider la recherche de solutions, de bonnes performances on été obtenues sur les problèmes continus. Dans un deuxième temps, une méthode générique de résolution de contraintes a été définie avec des outils d'IntAbs, afin d'intégrer les domaines abstraits existants. Le prototype, AbSolute, peut ainsi résoudre des problèmes mixtes et utiliser les domaines relationnels implémentés.
 

Vendredi 9 novembre 2018 de 10:30 à 12:00
Introduction à l'interpretation abstraite
MDSC

Type : Séminaire
Titre : Introduction à l'interpretation abstraite
Intervenant(s) :
Pellau Marie
Lieu d'exercice : laboratoire I3S
Date et lieu : Vendredi 9 novembre 2018 de 10:30 à 12:00 , Salle de conférence du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

Introduction à l'interpretation abstraite

Vendredi 19 octobre 2018 de 10:30 à 12:00
Langages à pile visible
MDSC

Type : Séminaire
Titre : Langages à pile visible
Intervenant(s) :
Etienne Lozes
Lieu d'exercice : I3S
Date et lieu : Vendredi 19 octobre 2018 de 10:30 à 12:00 , Salle de conférence du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

Introduction au working group et présentation de langages à pile visible