Publications

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