Source author record

Lucas C. Cordeiro

Lucas C. Cordeiro appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

9works
7topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2026arXiv

FedSurrogate: Backdoor Defense in Federated Learning via Layer Criticality and Surrogate Replacement

Federated Learning remains highly susceptible to backdoor attacks--malicious clients inject targeted behaviours into the global model. Existing defenses suffer from substantial false-positive rates under realistic non-independent and identically distributed (non-IID) data, incorrectly flagging benign clients and degrading model accuracy even when adversaries are correctly identified. We present FedSurrogate, a novel backdoor defense that addresses this limitation by combining bidirectional gradient alignment filtering with layer-adaptive anomaly detection. FedSurrogate performs selective clustering on security-critical layers identified via directional divergence analysis, concentrating the detection signal on a low-dimensional subspace. A bidirectional soft-filtering stage screens trusted clients for residual contamination while rescuing false positives from suspects, substantially reducing misclassifications under heterogeneous conditions. Rather than removing confirmed malicious updates, FedSurrogate replaces them with downscaled surrogate updates from structurally similar benign clients, preserving gradient diversity while neutralising adversarial influence. Extensive evaluations demonstrate that FedSurrogate maintains false-positive rates below 10% across all datasets and attack types, compared to 31-32% for the nearest comparably effective baseline, while achieving superior main-task accuracy and maintaining attack success rates below 2.1% across all tested datasets and attack types under challenging non-IID settings.

preprint2022arXiv

CEG4N: Counter-Example Guided Neural Network Quantization Refinement

Neural networks are essential components of learning-based software systems. However, their high compute, memory, and power requirements make using them in low resources domains challenging. For this reason, neural networks are often quantized before deployment. Existing quantization techniques tend to degrade the network accuracy. We propose Counter-Example Guided Neural Network Quantization Refinement (CEG4N). This technique combines search-based quantization and equivalence verification: the former minimizes the computational requirements, while the latter guarantees that the network's output does not change after quantization. We evaluate CEG4N~on a diverse set of benchmarks, including large and small networks. Our technique successfully quantizes the networks in our evaluation while producing models with up to 72% better accuracy than state-of-the-art techniques.

preprint2022arXiv

ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation

In this work, we describe and evaluate the first model checker for verifying Kotlin programs through the Jimple intermediate representation. The verifier, named ESBMC-Jimple, is built on top of the Efficient SMT-based Context-Bounded Model Checker (ESBMC). It uses the Soot framework to obtain the Jimple IR, representing a simplified version of the Kotlin source code, containing a maximum of three operands per instruction. ESBMC-Jimple processes Kotlin source code together with a model of the standard Kotlin libraries and checks a set of safety properties. Experimental results show that ESBMC-Jimple can correctly verify a set of Kotlin benchmarks from the literature and that it is competitive with state-of-the-art Java bytecode verifiers. A demonstration is available at https://youtu.be/J6WhNfXvJNc.

preprint2020arXiv

An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

We describe a new SMT bit-blasting API for floating-points and evaluate it using different out-of-the-shelf SMT solvers during the verification of several C programs. The new floating-point API is part of the SMT backend in ESBMC, a state-of-the-art bounded model checker for C and C++. For the evaluation, we compared our floating-point API against the native floating-point APIs in Z3 and MathSAT. We show that Boolector, when using floating-point API, outperforms the solvers with native support for floating-points, correctly verifying more programs in less time. Experimental results also show that our floating-point API implemented in ESBMC is on par with other state-of-the-art software verifiers. Furthermore, when verifying programs with floating-point arithmetic, our new floating-point API produced no wrong answers.

preprint2020arXiv

Verifying Software Vulnerabilities in IoT Cryptographic Protocols

Internet of Things (IoT) is a system that consists of a large number of smart devices connected through a network. The number of these devices is increasing rapidly, which creates a massive and complex network with a vast amount of data communicated over that network. One way to protect this data in transit, i.e., to achieve data confidentiality, is to use lightweight encryption algorithms for IoT protocols. However, the design and implementation of such protocols is an error-prone task; flaws in the implementation can lead to devastating security vulnerabilities. These vulnerabilities can be exploited by an attacker and affect users' privacy. There exist various techniques to verify software and detect vulnerabilities. Bounded Model Checking (BMC) and Fuzzing are useful techniques to check the correctness of a software system concerning its specifications. Here we describe a framework called Encryption-BMC and Fuzzing (EBF) using combined BMC and fuzzing techniques. We evaluate the application of EBF verification framework on a case study, i.e., the S-MQTT protocol, to check security vulnerabilities in cryptographic protocols for IoT.

preprint2016arXiv

Application of Global Route-Planning Algorithms with Geodesy

Global Route-Planning Algorithms (GRPA) are required to compute paths between several points located on Earth's surface. A geodesic algorithm is employed as an auxiliary tool, increasing the precision of distance calculations. This work presents a novel simulator for GRPA, which compares and evaluates three GRPAs implemented to solve the shortest path problem for points located at different cities: A*, LPA*, and D*Lite. The performance of each algorithm is investigated with a set of experiments, which are executed to check the answers provided by the algorithms and to compare their execution time. It is shown that GRPAs implementations with consistent heuristics lead to optimal paths. The noticeable differences among those algorithms are related to the time execution after successive executions.

preprint2016arXiv

Complementary Training Programme for Electrical and Computer Engineering Students Through an Industrial-Academic Collaboration (Extended Version)

We describe the results of an industrial-academic collaboration among the Graduate Program in Electrical Engineering (PPGEE), the Electronics and Information Research Centre (CETELI), and Samsung Eletrônica da Amazônia Ltda. (Samsung), which aims at training human resources for Samsung's research and development (R&D) areas. Inspired by co-operative education systems, this collaboration offers an academic experience by means of a complementary training programme (CTP), in order to train undergraduates and graduate students in electrical and computer engineering, with especial emphasis on digital television (TV), industrial automation, and mobile devices technologies. In particular, this cooperation has provided scholarships for students and financial support for professors and coordinators in addition to the construction of a new building with new laboratories, classrooms, and staff rooms, to assist all research and development activities. Additionally, the cooperation outcomes led to applications developed for Samsung's mobile devices, digital TV, and production processes, an increase of 37% in CETELI's scientific production (i.e., conference and journal papers) as well as professional training for undergraduates and graduate students.

preprint2015arXiv

Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)

The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification processes, in order to create robust systems and reduce product recall rates. Because of that, the present paper proposes a simplified version of the Qt framework, which is integrated into the Efficient SMT-Based Bounded Model Checking tool to verify actual applications that use the mentioned framework. The method proposed in this paper presents a success rate of 94.45%, for the developed test suite.

preprint2015arXiv

Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)

Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threaded program into a corresponding sequential one and then uses a fault-diagnosis method suitable for this type of program, in order to localize faults. The code transformation is implemented with rules and context switch information from counterexamples, which are typically generated by bounded model checkers. Experimental results show that the proposed method is effective, in such a way that sequential fault-localization methods can be extended to multi-threaded programs.