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

Liste des WG MDSC à venir

Friday 24 May 2019 14:00
Hoare calculus, Separation Logic and robustness properties of imperative programs.
MDSC

Titre de l'exposé : Hoare calculus, Separation Logic and robustness properties of imperative programs.
Type : Séminaire
Intervenant(s) :
Alessio Mansutti
Lieu d'exercice : LSV, Paris Saclay
Date de l'exposé : Friday 24 May 2019 14:00
Lieu de l'exposé : Salle de conférence du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

Separation logic is an extension of Hoare’s proof system which supports a local way of reasoning about programs that mutate memory. This talk starts with a short introduction on Hoare's calculus. We then discuss why this formalism lacks modularity and switch our attention to propositional separation logic (Reynolds, LICS'02). We take this opportunity to revisit one major result on propositional separation logic (Lozes, SPACE'04) and then briefly explain how it can be extended to a logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. The satisfiability problem of this logic is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard (Mansutti, FSTTCS'18).

Liste des WG MDSC passées

Tuesday 19 February 2019 14:30 to 15:30
An introduction to Session Types
MDSC

Type : Séminaire
Titre : An introduction to Session Types
Intervenant(s) :
Cinzia Di Giusto
Lieu d'exercice : I3S
Date et lieu : Tuesday 19 February 2019 14:30 to 15:30 , Salle de réunion du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

An introduction to process algebra and session types

Thursday 13 December 2018 10:30 to 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 : Thursday 13 December 2018 10:30 to 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.

Friday 7 December 2018 10:30 to 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 : Friday 7 December 2018 10:30 to 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.

Friday 23 November 2018 10:30 to 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 : Friday 23 November 2018 10:30 to 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.
 

Friday 9 November 2018 10:30 to 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 : Friday 9 November 2018 10:30 to 12:00 , Salle de conférence du laboratoire I3S à Sophia Antipolis
Résumé/Abstract:

Introduction à l'interpretation abstraite

Friday 19 October 2018 10:30 to 12:00
Langages à pile visible
MDSC

Type : Séminaire
Titre : Langages à pile visible
Intervenant(s) :
Etienne Lozes
Lieu d'exercice : I3S
Date et lieu : Friday 19 October 2018 10:30 to 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