1. SMTCoq: A plug-in for integrating SMT solvers into Coq

    Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds and Clark Barrett.
    In CAV, Heidelberg, Germany, July 2017.

    PDF BibTeX
  2. Qualification of a Model Checker for Avionics Software Verification

    Lucas G. Wagner, Alain Mebsout, Cesare Tinelli, Darren D. Cofer and Konrad Slind.
    In NFM, Moffett Field, California, USA, May 2017.

    PDF BibTeX
  3. Proof Certificates for SMT-based Model Checkers for Infinite State Systems

    Alain Mebsout and Cesare Tinelli.
    In FMCAD, Mountain View, California, USA, October 2016.

    PDF BibTeX
  4. The Kind 2 Model Checker

    Adrien Champion, Alain Mebsout, Christoph Sticksel and Cesare Tinelli.
    In CAV, Toronto, Ontario, Canada, July 2016.

    PDF BibTeX
  5. AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo

    Sylvain Conchon, Mohamed Iguernlala and Alain Mebsout.
    In UITP@IJCAR, Coimbra, Portugal, July 2016.

    PDF BibTeX
  6. Extending SMTCoq, a Certified Checker for SMT

    Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds and Cesare Tinelli.
    In HaTT@IJCAR, Coimbra, Portugal, July 2016.

    PDF BibTeX
  7. Certificates for Parameterized Model Checking

    Sylvain Conchon, Alain Mebsout and Fatiha Zaïdi.
    In FM, Oslo, Norway, June 2015.

    PDF BibTeX
  8. Inférence d'invariants pour le model checking de systèmes paramétrés (in french)

    Alain Mebsout.
    Ph.D. thesis, Université Paris-Sud, September 2014.

    Thesis Slides BibTeX
  9. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières (in french)

    Sylvain Conchon, David Declerck, Luc Maranget and Alain Mebsout.
    In JFLA, Fréjus, France, January 2014.

    PDF BibTeX
  10. Invariants for Finite Instances and Beyond

    Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi.
    In FMCAD, Portland, Oregon, USA, October 2013.

    PDF BibTeX
  11. A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo

    Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout.
    In SYNASC, Timișoara, Romania, September 2013.

    PDF BibTeX
  12. Vérification de systèmes paramétrés avec Cubicle (in french)

    Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi.
    In JFLA, Aussois, France, February 2013.

    PDF BibTeX
  13. Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems

    Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi.
    In CAV, Berkeley, California, USA, July 2012

    PDF BibTeX
  14. A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic

    François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
    In IJCAR, Manchester, UK, June 2012

    PDF BibTeX