L'apprentissage de clauses, dans le domaine du raisonnement par contrainte, a fait des progrès très importants au cours des deux dernières décennies. C'est un composant bien connu des solveurs SAT modernes, qui est également devenu un sujet de grand intérêt pour la mise en œuvre de solveurs CP robustes. Parmi les techniques fructueuses, qui se sont révélées efficaces sur une variété de problèmes, nous trouvons l'enregistrement de nogoods (généralisés), lazy clause generation (LCG) et l'apprentissage non clausal. Jusqu'à présent, les résultats pratiques les plus probants ont été obtenus en mettant en œuvre des procédures spécifiques en fonction de la nature des contraintes (par exemple, différentes manières d'expliquer les contraintes globales dans LCG, ou diverses règles permettant de déduire des contraintes de conflit dans l'inférence non clausale).

Dans ce séminaire, nous allons dans un premier temps discuter des cœurs modernes de solveurs CP puis nous revisitons l’apprentissage de clauses pour CSP, en exploitant quelques idées intéressantes introduites dans la littérature (telles que l’enregistrement de g-nogood, LCG et l’analyse de conflits dans le contexte de graphes) ainsi que leur efficacité au sein du solveur NACRE et proposons de nouvelles techniques génériques afin de rendre l’apprentissage par clause non intrusif et efficace pour CSP.

We present a type-based analysis to ensure memory safety and object protocol completion in a Java-like language. The analysis prevents not only null pointer dereferencing and memory leaks, but also that the intended usage protocol of each object is respected and completed.

Modern society is increasingly dependent on large-scale software systems that are distributed, collaborative, and communication-centred. To verify software products for such systems, we have to make sure that the modelling languages exactly capture the system requirements on that its implementation relies. For this purpose we present synchronisation patterns that capture different degrees of synchrony in interactions and allow to classify the expressive power of modelling languages. With that we can identify process calculi (or other formalisms) that do not contain any synchronisation mechanisms and are fully distributed, we can identify hidden (and unexpected) kinds of synchronisation, and we can analyse the degree of synchronisation that can be expressed by a language.

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).

An introduction to process algebra and session types

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.

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.

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.
 

Introduction à l'interpretation abstraite

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