Publications : Alain Mebsout
Retour[11]  Ç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 248250, 2022. [ bib  full text on HAL ] 
[10]  Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. AltErgo 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é ParisSud, 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 Vingtcinquiè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 6168, Portland, Oregon, ÉtatsUnis,
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 stateoftheart 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 overapproximations 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 Vingtquatriè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 nonlinear integer arithmetic reasoning in AltErgo. 2013. [ bib  full text on HAL ] 
[4]  Sylvain Conchon, Mohamed Iguernelala, and Alain Mebsout. A collaborative framework for nonlinear integer arithmetic reasoning in altergo. In 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 161168, 2013. [ bib  DOI ] 
[3] 
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha
Zaïdi.
Cubicle: A parallel SMTbased 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 stateoftheart model checkers.

[2] 
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala,
Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
A Simplexbased extension of FourierMotzkin 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 6781, Manchester, UK, June 2012. Springer.
[ bib 
DOI 
full text on HAL ]
This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. OmegaTest) or by branching/cutting methods (branchandbound, branchandcut, 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 AltErgo theorem prover. Experimental results are promising and show that our approach is competitive with stateoftheart SMT solvers.

[1]  François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The AltErgo automated theorem prover, 2008. http://altergo.lri.fr/. [ bib ] 
Retour
This page was generated by bibtex2html.