Zobrazeno 1 - 10
of 21
pro vyhledávání: '"François, Bobot"'
Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer
Externí odkaz:
http://arxiv.org/abs/1811.12515
Autor:
Julien Signoles, Nikolai Kosmatov, David Bühler, Virgile Prevosto, Patrick Baudin, Loïc Correnson, Valentin Perrelle, Florent Kirchner, François Bobot, André Maroneze, Nicky Williams
Publikováno v:
Communications of the ACM. 64:56-68
A panoramic view of a popular platform for C program analysis and verification.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d49789ccec3fecdcdb11b1f388e4735a
https://doi.org/10.1145/3470569
https://doi.org/10.1145/3470569
Autor:
François Bobot, Aaron Dutle, Gregory Anderson, César A. Muñoz, Laura Titolo, Mariano M. Moscato
Publikováno v:
Formal Aspects of Computing. 33:65-86
The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate current state information, including position and velocity messages, to other aircraft in their vicinity and to ground stations. The Compact Position Reporti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2e3e0ca0e88b9eeb85c33c1332f476f5
https://doi.org/10.1007/s00165-019-00504-0
https://doi.org/10.1007/s00165-019-00504-0
Autor:
Zeinab Nehaï, François Bobot, Sara Tucci-Piergiovanni, Carole Delporte-Gallet, Hugues Fauconnier
Publikováno v:
Proceedings of the 23rd International Conference on Distributed Computing and Networking.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a70c7af85a4001c91abd6dc16f64f77e
https://doi.org/10.1145/3491003.3491006
https://doi.org/10.1145/3491003.3491006
Publikováno v:
Programming Languages and Systems ISBN: 9783030720186
ESOP
ESOP
While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::150cb4251ccc1bd9b9b324f4c2c6bb94
https://doi.org/10.1007/978-3-030-72019-3_6
https://doi.org/10.1007/978-3-030-72019-3_6
Autor:
François Bobot, Zeinab Nehai
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030549930
FM Workshops (1)
FM Workshops (1)
In this paper, we use a formal tool that performs deductive verification on industrial smart contracts, which are self-executing digital programs. Because smart contracts manipulate cryptocurrency and transaction information, if a bug occurs in such
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9082ec246f9cb74b0e75e466c2b41538
https://doi.org/10.1007/978-3-030-54994-7_22
https://doi.org/10.1007/978-3-030-54994-7_22
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030112448
VMCAI
VMCAI
Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5cb759c462496c8b30143b2f19ff2a28
https://doi.org/10.1007/978-3-030-11245-5_8
https://doi.org/10.1007/978-3-030-11245-5_8
Publikováno v:
Formal Methods ISBN: 9783319955810
FM
FM
The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate their current state, including position and velocity information, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a019fef89281878c186358dc7eae7c80
https://doi.org/10.1007/978-3-319-95582-7_22
https://doi.org/10.1007/978-3-319-95582-7_22
Publikováno v:
The SMT Workshop
The SMT Workshop, SMT 2017, 15th International Workshop on Satisfiability Modulo Theories, Jul 2017, Heidelberg, Germany
Scopus-Elsevier
The SMT Workshop, SMT 2017, 15th International Workshop on Satisfiability Modulo Theories, Jul 2017, Heidelberg, Germany
Scopus-Elsevier
International audience; We present an efficient constraint programming (CP) approach to the SMTLIB theory of quantifier-free floating-point arithmetic (QF FP). We rely on dense interreduction between many domain representations to greatly reduce the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::391313e813d7b0ab9159563f0d516a0e
https://hal-cea.archives-ouvertes.fr/cea-01795760/file/main.pdf
https://hal-cea.archives-ouvertes.fr/cea-01795760/file/main.pdf
Publikováno v:
CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems
CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Jun 2017, Padova, Italy
Integration of AI and OR Techniques in Constraint Programming ISBN: 9783319597751
CPAIOR
CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Jun 2017, Padova, Italy
Integration of AI and OR Techniques in Constraint Programming ISBN: 9783319597751
CPAIOR
International audience; We address the challenge of developing efficient Constraint Programming-based approaches for solving formulas over the quantifier-free fragment of the theory of bitvectors (BV), which is of paramount importance in software ver
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2ab63d18cde8cd6227442464a51bd9e3
https://cea.hal.science/cea-01795779/file/bv-cpaior.pdf
https://cea.hal.science/cea-01795779/file/bv-cpaior.pdf