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}
}
@inproceedings{bozman22jfla,
topics = {team},
title = {Jouez {\`a} Faire Consensus Avec {MITTEN} (d{\'e}monstration)},
author = {Bozman, {\c C}agdas and Iguernlala, Mohamed and Laporte, Michael and Levillain, Maxime and Mebsout, Alain and Conchon, Sylvain},
hal = {https://hal.inria.fr/hal-03626847},
booktitle = {33{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
editor = {Chantal Keller and Timothy Bourke},
pages = {248--250},
year = 2022
}
@inproceedings{conchon21fmbc,
topics = {team},
author = {Sylvain Conchon and Alexandrina Korneva and {\c{C}}agdas Bozman and
Mohamed Iguernlala and Alain Mebsout},
editor = {Bruno Bernardo and Diego Marmsoler},
title = {Formally Documenting Tenderbake (Short Paper)},
booktitle = {3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV
2021, July 18-19, 2021, Los Angeles, California, {USA} (Virtual Conference)},
series = {OASIcs},
volume = 95,
pages = {4:1--4:9},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = 2021,
doi = {10.4230/OASICS.FMBC.2021.4}
}
@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}
}