activity
20092021
most citedOptimal Sizing of Stand-alone Solar PV Systems via Automated Formal Synthesis

3 citations · 13 across the 15 of their papers we have counts for

collaborators

23 papers

cs.SE2021

Model Checking C++ Programs

Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro

In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the significant sources of security vulnerabilities. However, ther…

cs.LG20211 cited

Verifying Quantized Neural Networks using SMT-Based Model Checking

Luiz Sena, Xidan Song, Erickson Alves +4

Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis. However, concerns ab…

cs.CR2021

Finding Security Vulnerabilities in IoT Cryptographic Protocol and Concurrent Implementations

Fatimah Aljaafari, Rafael Menezes, Mustafa A. Mustafa +1

Internet of Things (IoT) consists of a large number of devices connected through a network, which exchange a high volume of data, thereby posing new security, privacy, and trust is…

cs.CR2021

Verifying Security Vulnerabilities in Large Software Systems using Multi-Core k-Induction

Thales Silva, Carmina Porto, Erickson Alves +2

Computer-based systems have been used to solve several domain problems, such as industrial, military, education, and wearable. Those systems need high-quality software to guarantee…

cs.CR20201 cited

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs

Kaled M. Alshmrany, Rafael S. Menezes, Mikhail R. Gadelha +1

We describe and evaluate a novel white-box fuzzer for C programs named FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find secu…

cs.LO2020

Incremental Verification of Fixed-Point Implementations of Neural Networks

Luiz Sena, Erickson Alves, Iury Bessa +2

Implementations of artificial neural networks (ANNs) might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are…