AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo

Autor: Conchon, Sylvain, Iguernlala, Mohamed, Mebsout, Alain

Publikováno v: EPTCS 239, 2017, pp. 1-13

Due to undecidability and complexity of first-order logic, SMT solvers may not terminate on some problems or require a very long time. When this happens, one would like to find the reasons why the solver fails. To this end, we have designed AltGr-Erg

Externí odkaz: http://arxiv.org/abs/1701.07124

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

Autor: Ekici, Burak, Katz, Guy, Keller, Chantal, Mebsout, Alain, Reynolds, Andrew J., Tinelli, Cesare

Publikováno v: EPTCS 210, 2016, pp. 21-29

This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq

Externí odkaz: http://arxiv.org/abs/1606.05947

Formally Documenting Tenderbake

Autor: Conchon, Sylvain, Korneva, Alexandrina, Bozman, Çagdas, Iguernlala, Mohamed, Mebsout, Alain

Publikováno v: Open Access Series in Informatics
Open Access Series in Informatics, Schloss Dagstuhl-Leibniz-Zentrum für Informatik, In press, ⟨10.4230/OASIcs.FMBC.2021.5⟩
Open Access Series in Informatics, In press, ⟨10.4230/OASIcs.FMBC.2021.5⟩

International audience; In this paper, we propose a formal documentation of Tenderbake, the new Tezos consensus algorithm, slated to replace the current Emmy family algorithms. The algorithm is broken down to its essentials and represented as an auto

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::f04c26f07a20fd99c411fc662b008d2a
https://hal.archives-ouvertes.fr/hal-03398884/file/main.pdf

Alt-Ergo 2.2

Autor: Conchon, Sylvain, Coquereau, Albin, Iguernlala, Mohamed, Mebsout, Alain

Publikováno v: SMT Workshop: International Workshop on Satisfiability Modulo Theories
SMT Workshop: International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom

International audience; Alt-Ergo is an SMT solver jointly developed by Université Paris-Sud and the OCamlPro company. The first version was released in 2006. Since then, its architecture has been continuously adapted for proving formulas generated b

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______2592::abc4f5d5d03758132720b0f1134df945
https://hal.inria.fr/hal-01960203/document

Invariants inference for model checking of parameterized systems

Autor: Mebsout, Alain

Publikováno v: Autre [cs.OH]. Université Paris Sud-Paris XI, 2014. Français. ⟨NNT : 2014PA112188⟩

This thesis tackles the problem of automatically verifying complexparameterized systems. This approach is important because it can guarantee thatsome properties hold without knowing a priori the number of components in thesystem. We focus in particul

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::d4898bf745a6f610eeec04bf43360b79
https://tel.archives-ouvertes.fr/tel-01073980/file/VA2_MEBSOUT_ALAIN_29092014.pdf