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