mebsout.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc mebsout.cite -ob mebsout.bib -c 'author : "mebsout"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@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{conchon12cav,
  author = {Sylvain Conchon and Amit Goel and Sava Krsti{\'c}
                  and Alain Mebsout and Fatiha Za{\"i}di},
  title = {{Cubicle}: A Parallel {SMT}-based Model Checker for
                  Parameterized Systems},
  booktitle = {CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification},
  year = {2012},
  topics = {team},
  hal = {http://hal.archives-ouvertes.fr/hal-00799272},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL Fortesse ext},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CAV},
  editor = {Madhusudan Parthasarathy and Sanjit A. Seshia},
  series = {Lecture Notes in Computer Science},
  volume = 7358,
  month = jul,
  address = {Berkeley, California, USA},
  publisher = {Springer},
  abstract = { Cubicle is a new model checker for verifying safety
                  properties of parameterized systems. It implements a
                  parallel symbolic backward reachability procedure
                  using Satisfiabilty Modulo Theories.  Experiments
                  done on classic and challenging mutual exclusion
                  algorithms and cache coherence protocols show that
                  Cubicle is effective and competitive with
                  state-of-the-art model checkers.}
}
@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{conchon13jfla,
  author = {Sylvain Conchon and Alain Mebsout and Fatiha Za\"{\i}di},
  title = {V\'erification de syst\`emes param\'etr\'es avec {Cubicle}},
  crossref = {jfla13},
  topics = {team},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL Fortesse},
  x-type = {article},
  x-support = {actes},
  hal = {http://hal.inria.fr/hal-00778832}
}
@inproceedings{conchon13fmcad,
  topics = {team},
  hal = {http://hal.archives-ouvertes.fr/hal-00924640},
  title = {Invariants for Finite Instances and Beyond},
  author = {Conchon, Sylvain and Goel, Amit and Krsti{\'c}, Sava and Mebsout, Alain and Za{\"\i}di, Fatiha},
  abstract = {Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.},
  booktitle = {FMCAD},
  pages = {61--68},
  address = {Portland, Oregon, {\'E}tats-Unis},
  audience = {internationale},
  doi = {10.1109/FMCAD.2013.6679392},
  year = 2013,
  month = oct
}
@phdthesis{mebsout14phd,
  title = {Invariants inference for model checking of parameterized systems},
  author = {Mebsout, Alain},
  hal = {https://tel.archives-ouvertes.fr/tel-01073980},
  topics = {team},
  school = {Universit{\'e} Paris-Sud},
  year = 2014,
  month = sep,
  type = {Th{\`e}se de Doctorat}
}
@inproceedings{conchon14jfla,
  hal = {https://hal.inria.fr/hal-01088655},
  topics = {team},
  author = {Sylvain Conchon and David Declerck and Luc Maranget and Alain Mebsout},
  title = {Vérification de programmes {C} concurrents avec {Cubicle} : Enfoncer les barrières},
  crossref = {jfla14}
}
@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}
}
@inproceedings{conchon18smt,
  topics = {team},
  title = {{Alt-Ergo} 2.2},
  author = {Conchon, Sylvain and Coquereau, Albin and  Iguernlala, Mohamed and Mebsout, Alain},
  hal = {https://hal.inria.fr/hal-01960203},
  booktitle = {SMT Workshop: International Workshop on Satisfiability Modulo Theories},
  address = {Oxford, United Kingdom},
  year = 2018,
  month = jul,
  pdf = {https://hal.inria.fr/hal-01960203/file/Alt-Ergo-2.2--SMT-Workshop-2018.pdf},
  hal_id = {hal-01960203},
  hal_version = {v1}
}
@proceedings{jfla13,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2013,
  booktitle = {Vingt-quatri\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = feb,
  address = {Aussois, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{jfla14,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2014,
  booktitle = {Vingt-cinqui\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Fr\'ejus, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}