Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de IGUERNELALA Mohamed
IGUERNELALA Mohamed
Ph.D
Group :

Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures

Starts on 01/10/2009
Advisor : CONCHON, Sylvain

Funding :
Affiliation : Université Paris-Sud
Laboratory : LRI / INRIA-SACLAY

Defended on 10/06/2013, committee :
M. Frédéric Besson - Examinateur
M. Sylvain Conchon - Encadrant, directeur de thèse
Mme Evelyne Contejean - Co-encadrante
M. Florent Hivert - Examinateur
M. Michaël Rusinowitch - Rapporteur
M. Ralf Treinen - Examinateur

Research activities :
   - Automated Proof, SMT and Applications

Abstract :
This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.

SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.

This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutative symbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.

Ph.D. dissertations & Faculty habilitations
APPRENTISSAGE ET OPTIMISATION SUR LES GRAPHES


ANALYSE DE DONNéES MULTI-MODALES POUR LES PATHOLOGIES COMPLEXES PAR LA CONCEPTION ET L’IMPLéMENTATION DE PROTOCOLES REPRODUCTIBLES ET RéUTILISABLES


DESIGNING INTERACTIVE TOOLS FOR CREATORS AND CREATIVE WORK
Creative work has been at the core of research in Human-Computer Interaction (HCI). I describe the results of a series of studies that look at how creators work, where creators include artists with years of professional practice, as well as learners, or novices and casual makers. My research focuses on three creation activities: drawing, physical modeling, and music composition. For these activities, I examine how artists switch between representations and how these representations evolve throughout their creative process, from early sketches to fine-grained forms or structured vocabularies. I present interactive systems that enrich their workflow (i) by extending their computer tools with physical user interfaces, or (ii) by making physical materials interactive. I also argue that sketch-based representations can allow for user interfaces that are more personal and less rigid. My presentation will reflect on lessons and limitations of this work and discuss challenges for future design-support tools.