LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » News » PhD students

METIN Hakan

PhD student (Teaching assistant, Sorbonne Université)
Team : MoVe
Arrival date : 10/01/2016
Localisation : Campus Pierre et Marie Curie
    Sorbonne Université - LIP6
    Boîte courrier 169
    Couloir 25-26, Étage 2, Bureau 231
    4 place Jussieu
    75252 PARIS CEDEX 05
    FRANCE
Tel: +33 1 44 27 51 28, Hakan.Metin (at) nulllip6.fr
https://pages.lip6.fr/Hakan.Metin
Supervision : Fabrice KORDON
Co-supervision : BAARIR Souheib

Exploitation des symétries dynamiques pour la résolution des problèmes SAT

Avec l’intégration toujours plus grande, des systèmes informatiques dans des applications critiques (métro, voitures, centrales-nucléaires, blocs opératoires, etc), assurer la correction des programmes devient une nécessité. Si l’utilisation systématique de tests permet d’améliorer grandement la qualité du code, elle ne peut réellement garantir leur correction. A l’inverse, les techniques dites de model-checking, qui vérifient la validité du workflow applicatif (modélisé par un graphe d’états) par rapport à une propriété donnée, permettent de garantir la correction des programmes. Ces techniques reposent, essentiellement, sur deux théories : celle basée sur les automates et celle fondée sur la satisfiabilité booléenne (SAT). Dans les deux théories l’ennemi commun est le problème bien connu de l’explosion combinatoire. En utilisant les automates, le problème se manifeste par une consommation mémoire démesurée, alors qu’en utilisant le SAT, le problème se manifeste sous la forme d’un temps de calcul extrêmement long. Cependant, certains systèmes exhibent des comportements symétriques, i.e., les compo- sants du système se comportent de façon identique à une permutation des identités près. Ces symétries se traduisent naturellement sur les problèmes SAT générés lors de la vérification : en effet, les permutations détectées au niveau du système se traduisent (de façon triviale) par des permutations, dont l’application laisse la formule SAT invariante. Ainsi, la prise en compte de symétries lors la résolution du problème est censée réduire considérablement le temps de calcul !

2018-2019 Publications

  • 2019
  • 2018
    • H. Metin, S. Baarir, M. Colange, F. Kordon : “CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving”, Tools and Algorithms for the Construction and Analysis of Systems -- TACAS, Tools and Algorithms for the Construction and Analysis of Systems 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proce, Tessaloniki, Greece (2018)
    • S. Baarir, R. Bendraou, H. Metin, Y. Laurent : “ProVer: an SMT-based approach for process verification”, Model-Driven Engineering Verification & Validation, MoDELS Workshop, vol. 2245, MODELS Workshops, Copenhague, Denmark, pp. 555-562 (2018)
 Mentions légales
Site map |