Zobrazeno 1 - 10
of 20
pro vyhledávání: '"Mikhail R. Gadelha"'
Autor:
Mohannad Aldughaim, Kaled M. Alshmrany, Mikhail R. Gadelha, Rosiane de Freitas, Lucas C. Cordeiro
Publikováno v:
Fundamental Approaches to Software Engineering ISBN: 9783031308253
The cooperative verification of Bounded Model Checking and Fuzzing has proved to be one of the most effective techniques when testing C programs. FuSeBMC is a test-generation tool that employs BMC and Fuzzing to produce test cases. In Test-Comp 2023,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::78ddd908ba8a29bd59f838cac03ef835
https://doi.org/10.1007/978-3-031-30826-0_18
https://doi.org/10.1007/978-3-031-30826-0_18
Autor:
Franz Brauße, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro
Publikováno v:
Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a8bc1b10d6d2ba24acece778ded808d9
https://doi.org/10.1145/3533767.3543289
https://doi.org/10.1145/3533767.3543289
Publikováno v:
2022 IEEE Conference on Software Testing, Verification and Validation (ICST).
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2d63de31dc01fd7133c1819f55fc3deb
https://doi.org/10.1109/icst53961.2022.00054
https://doi.org/10.1109/icst53961.2022.00054
Publikováno v:
International Journal on Software Tools for Technology Transfer. 23:857-861
ESBMC is an SMT-based bounded model checker that provides a bit-precise verification of both C and C++ programs. Bounded model checking (BMC) was developed to provide faster results when finding property violations; BMC achieves this by limiting the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::04e173e785a5b2347dc74d6dbc6497de
https://doi.org/10.1007/s10009-020-00571-2
https://doi.org/10.1007/s10009-020-00571-2
Autor:
Sergio Cleger Tamayo, Everton Lima Aleixo, Everlandio Fernandes, Mikhail R. Gadelha, Aasim Khurshid, Wesley Jacinto Barreira
Publikováno v:
Artificial Intelligence in HCI ISBN: 9783030777715
HCI (36)
HCI (36)
In this study, we explore recent advances in photorealistic style transfer methods to make visual predictions of outdoor scenes. These methods transfer the elements’ visual appearance from one photo (style image) to another (content image), maintai
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b204b890bd146445522ae7defc82ad61
https://doi.org/10.1007/978-3-030-77772-2_20
https://doi.org/10.1007/978-3-030-77772-2_20
Publikováno v:
Fundamental Approaches to Software Engineering ISBN: 9783030714994
FASE
FASE
We describe and evaluate a novel white-box fuzzer for C programs named , which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. explores and analyzes C programs (1) to f
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::32e88e1a0a7f7e4ca9f4d86be6da09a2
https://doi.org/10.1007/978-3-030-71500-7_19
https://doi.org/10.1007/978-3-030-71500-7_19
Autor:
Mikhail R. Gadelha, Adriano M. Gil, Aasim Khurshid, Felipe Augusto Souza Guimarães, Everlandio Fernandes
Publikováno v:
Anais Estendidos da Conference on Graphics, Patterns and Images (SIBRAPI Estendido 2020).
The smartphone themes submitted to the themestore are first evaluated by human experts to ensure a pleasant visual experience1. One of the main challenges in smartphone themes evaluation is to validate the contrast of the elements of the theme. Contr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::58bd4863e0649efdebafa7e083bddc23
https://doi.org/10.5753/sibgrapi.est.2020.13015
https://doi.org/10.5753/sibgrapi.est.2020.13015
Publikováno v:
Alhawi, O, Rocha, H, Gadelha, M R, Cordeiro, L & Batista, E 2020, ' Verification and Refutation of C Programs based on k-Induction and Invariant Inference ', International Journal on Software Tools for Technology Transfer, vol. 23, pp. 115-135 . https://doi.org/10.1007/s10009-020-00564-1
DepthK is a source-to-source transformation tool that employs bounded model checking (BMC) to verify and falsify safety properties in single- and multi-threaded C programs, without manual annotation of loop invariants. Here, we describe and evaluate
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3afba2023b006c9660e2229be822e6f6
https://doi.org/10.1007/s10009-020-00564-1
https://doi.org/10.1007/s10009-020-00564-1
Autor:
Adélia Ferreira, Daydlene Gonçalves, Bianca Hayek Bianco, Mikhail R. Gadelha, Adriano M. Gil, Juliana Postal
Publikováno v:
HCI International 2020 – Late Breaking Papers: Universal Access and Inclusive Design ISBN: 9783030601485
HCI (44)
HCI (44)
Several smartphone vendors now offer theme stores where one can submit themes that change the appearance of the OS. Theme designer must follow policies and guidelines to have their themes accepted. One common issue is the low contrast of elements in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7e0a5b494286bf4dd8458085c1264856
https://doi.org/10.1007/978-3-030-60149-2_21
https://doi.org/10.1007/978-3-030-60149-2_21
Publikováno v:
Fundamental Approaches to Software Engineering ISBN: 9783030452339
FASE
FASE
ESBMC is an SMT-based bounded model checker for real-world C programs. Such programs often represent real numbers using the floating-points, most commonly, the IEEE floating-point standard (IEEE 754-2008). Thus, ESBMC now includes a new floating-poin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a7c7ef47687de2d2d9764e163db2b70f
https://doi.org/10.1007/978-3-030-45234-6_27
https://doi.org/10.1007/978-3-030-45234-6_27