iguernelala.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc iguernelala.cite -ob iguernelala.bib -c 'author : "iguernelala"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@techreport{conchon10rr,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
institution = {{LRI, Universit\'e Paris Sud}},
year = 2010,
type = {Research Report},
number = 1538,
month = dec,
topics = {team, lri},
type_publi = {interne},
type_digiteo = {no},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {rapport},
x-pdf = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
url = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
abstract = {http://www.lri.fr/~contejea/publis/rr1538/abstract.html}
}
@inproceedings{conchon11tacas,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
crossref = {tacas2011},
year = 2011,
month = apr,
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {TACAS},
url = {http://proval.lri.fr/publications/conchon11tacas.pdf},
hal = {http://hal.inria.fr/hal-00777663},
pages = {45-59},
doi = {10.1007/978-3-642-19835-9_6},
abstract = {http://www.lri.fr/~contejea/publis/2011tacas/abstract.html}
}
@article{conchon12lmcs,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {Canonized Rewriting and Ground {AC} Completion Modulo {Shostak} Theories : Design and Implementation},
journal = {Logical Methods in Computer Science},
year = {2012},
month = sep,
pages = {1--29},
volume = 8,
number = 3,
hal = {http://hal.inria.fr/hal-00798082},
url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1037&layout=abstract&iid=40},
topics = {team},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-international-audience = {yes},
x-editorial-board = {yes},
x-cle-support = {LMCS},
doi = {10.2168/LMCS-8(3:16)2012},
note = {Selected Papers of the Conference \emph{Tools and Algorithms for the Construction and Analysis of Systems} (TACAS 2011), Saarbr{\"u}cken, Germany, 2011}
}
@inproceedings{conchon10lpar,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Ground Associative and Commutative Completion Modulo Shostak Theories}},
booktitle = {LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
year = 2010,
editor = {Andrei Voronkov},
series = {EasyChair Proceedings},
address = {Yogyakarta, Indonesia},
month = oct,
note = {(short paper)},
type_publi = {colloque},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {LPAR}
}
@mastersthesis{iguernelala09master,
author = {Mohamed Iguernelala},
title = {{Extension modulo Associativit\'e-Commutativit\'e
de l'algorithme de cl\^oture par congruence CC(X)}},
school = {Universit{\'e} Paris-Sud},
year = 2009,
topics = {team},
type_publi = {rapport},
x-equipes = {demons PROVAL},
x-type = {master},
x-support = {rapport}
}
@misc{alt-ergo,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala and St\'ephane Lescuyer and Alain Mebsout},
title = {The {Alt-Ergo} Automated Theorem Prover},
note = {\url{http://alt-ergo.lri.fr/}},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL}
}
@inproceedings{bobot12ijcar,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and
\'Evelyne Contejean and Mohamed Iguernelala and
Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
title = {A {Simplex}-Based Extension of {Fourier-Motzkin} for
Solving Linear Integer Arithmetic},
booktitle = {IJCAR 2012: Proceedings of the 6th International Joint
Conference on Automated Reasoning},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
series = {Lecture Notes in Computer Science},
address = {Manchester, UK},
month = jun,
volume = {7364},
pages = {67--81},
hal = {http://hal.inria.fr/hal-00687640},
doi = {10.1007/978-3-642-31365-3_8},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
type_publi = {icolcomlec},
publisher = {Springer},
abstract = {This paper describes a novel decision procedure for
quantifier-free linear integer arithmetic. Standard
techniques usually relax the initial problem to the
rational domain and then proceed either by
projection (e.g. Omega-Test) or by branching/cutting
methods (branch-and-bound, branch-and-cut, Gomory
cuts). Our approach tries to bridge the gap between
the two techniques: it interleaves an exhaustive
search for a model with bounds inference. These
bounds are computed provided an oracle capable of
finding constant positive linear combinations of
affine forms. We also show how to design an
efficient oracle based on the Simplex procedure. Our
algorithm is proved sound, complete, and terminating
and is implemented in the Alt-Ergo theorem
prover. Experimental results are promising and show
that our approach is competitive with
state-of-the-art SMT solvers.}
}
@inproceedings{conchon12smt,
author = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and Mohamed Iguernelala},
title = {Built-in Treatment of an Axiomatic Floating-Point Theory for {SMT} Solvers},
pages = {12--21},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-cle-support = {SMT},
x-type = {article},
crossref = {smt2012},
topics = {team}
}
@phdthesis{iguer13phd,
author = {Mohamed Iguernelala},
title = {Strengthening the Heart of an {SMT}-Solver: Design and Implementation of Efficient Decision Procedures},
school = {Universit{\'e} Paris-Sud},
type = {Th{\`e}se de Doctorat},
hal = {http://tel.archives-ouvertes.fr/tel-00842555},
x-equipes = {demons ProVal Toccata},
x-support = {rapport},
x-type = {these},
topics = {team},
year = 2013,
month = jun
}
@inproceedings{conchon14abz,
topics = {team},
hal = {https://hal.inria.fr/hal-01093000},
author = {Sylvain Conchon and Mohamed Iguernelala},
title = {Tuning the {Alt-Ergo} {SMT} Solver for {B} Proof Obligations},
pages = {294--297},
year = 2014,
crossref = {abz2014},
doi = {10.1007/978-3-662-43652-3_27}
}
@unpublished{conchon:hal-00924646,
title = {A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in {Alt-Ergo}},
author = {Conchon, Sylvain and Iguernelala, Mohamed and Mebsout, Alain},
year = 2013,
hal = {https://hal.archives-ouvertes.fr/hal-00924646}
}
@inproceedings{conchon13synasc,
topics = {team},
author = {Conchon, Sylvain and Iguernelala, Mohamed and Mebsout, Alain},
title = {A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo},
year = 2013,
doi = {10.1109/SYNASC.2013.29},
booktitle = {15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
pages = {161--168}
}
@proceedings{tacas2011,
title = {Tools and Algorithms for the Construction and Analysis of Systems},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
year = 2011,
month = apr,
editor = {Parosh A. Abdulla and K. Rustan M. Leino},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6605},
isbn = {978-3-642-19834-2},
address = {Saarbr{\"u}cken, Germany}
}
@proceedings{smt2012,
booktitle = {SMT workshop},
editor = {Pascal Fontaine and Amit Goel},
publisher = {LORIA},
url = {http://smt2012.loria.fr/},
year = 2012,
x-international-audience = {yes},
x-proceedings = {no},
address = {Manchester, UK}
}
@proceedings{abz2014,
booktitle = {Abstract State Machines, Alloy, B, VDM, and Z (ABZ)},
publisher = {Springer},
address = {Toulouse, France},
volume = 8477,
series = {Lecture Notes in Computer Science},
audience = {internationale},
year = 2014,
month = jun
}