Wiki Agenda Contact English version

Publications : Alain Mebsout

Retour
[12] Çagdas Bozman, Mohamed Iguernlala, Michael Laporte, Maxime Levillain, Alain Mebsout, and Sylvain Conchon. Jouez à faire consensus avec MITTEN (démonstration). In Chantal Keller and Timothy Bourke, editors, 33èmes Journées Francophones des Langages Applicatifs, pages 248--250, 2022. [ bib | full text on HAL ]
[11] Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout. Formally documenting tenderbake (short paper). In Bruno Bernardo and Diego Marmsoler, editors, 3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021, July 18-19, 2021, Los Angeles, California, USA (Virtual Conference), volume 95 of OASIcs, pages 4:1--4:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [ bib | DOI ]
[10] Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. Alt-Ergo 2.2. In SMT Workshop: International Workshop on Satisfiability Modulo Theories, Oxford, United Kingdom, July 2018. [ bib | full text on HAL | .pdf ]
[9] Alain Mebsout. Invariants inference for model checking of parameterized systems. Thèse de doctorat, Université Paris-Sud, September 2014. [ bib | full text on HAL ]
[8] Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. In Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. [ bib | full text on HAL ]
[7] Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. Invariants for finite instances and beyond. In FMCAD, pages 61--68, Portland, Oregon, États-Unis, October 2013. [ bib | DOI | full text on HAL ]
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.

[6] Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. In Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013. [ bib | full text on HAL ]
[5] Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout. A collaborative framework for non-linear integer arithmetic reasoning in Alt-Ergo. 2013. [ bib | full text on HAL ]
[4] Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout. A collaborative framework for non-linear integer arithmetic reasoning in alt-ergo. In 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 161--168, 2013. [ bib | DOI ]
[3] Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi. Cubicle: A parallel SMT-based model checker for parameterized systems. In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification, volume 7358 of Lecture Notes in Computer Science, Berkeley, California, USA, July 2012. Springer. [ bib | full text on HAL ]
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.

[2] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, IJCAR 2012: Proceedings of the 6th International Joint Conference on Automated Reasoning, volume 7364 of Lecture Notes in Computer Science, pages 67--81, Manchester, UK, June 2012. Springer. [ bib | DOI | full text on HAL ]
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.

[1] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008. http://alt-ergo.lri.fr/. [ bib ]

Retour
This page was generated by bibtex2html.