LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Seminar
When Constraint Programming Meets Abstract Interpretation
- Date
- 22.10.2019, 11:00
- Place
- Pavillon des Jardins
- Speaker
- Charlotte Truchet (Universite de Nantes)
Constraint Programming aims at modeling and solving combinatorial problems. The problems are expressed as logical relations (the constraints) holding on variables which can take their values in given (often finite) domains. The constraints come with propagation algorithms, which implement a certain level of reasoning on their semantic in order to remove useless values from the domains, hence, they reduce the search space without loosing solutions. Constraint solvers apply these algorithms as far as possible, but this is usually not enough to actually find solutions: in this case, a solver typically adds hypotheses to the original problems and iterates. CP thus offers a variety of tools to solve a large variety of constraints (holding on cardinality, graphs, words, geometry…). Yet, mixing different variable types (such as real and integer) or different solving tools, while keeping the solvers properties, is still a challenge. In this talk, I will present the AbSolute solvers, which is built on abstract domains as defined in Abstract Interpretation, and naturally mixes different domains while keeping the solver properties (soundness, completeness). I will detail the Octagon and Polyhedra abstract domains as an example of relational domains, and explore their connections with other families of solving methods.