5 citations · 7 across the 8 of their papers we have counts for
8 papers
ESBMC-Python: A Bounded Model Checker for Python Programs
Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho +2
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pi…
Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking
Janislley Oliveira de Sousa, Bruno Carvalho de Farias, Thales Araujo da Silva +2
Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to g…
ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts
Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho +1
Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone…
QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
Xidan Song, Edoardo Manino, Luiz Sena +5
QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The…
Verification of Magnitude and Phase Responses in Fixed-Point Digital Filters
Daniel P. M. de Mello, Mauro L. de Freitas, Lucas C. Cordeiro +4
In the digital signal processing (DSP) area, one of the most important tasks is digital filter design. Currently, this procedure is performed with the aid of computational tools, w…
Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)
Erickson H. da S. Alves, Lucas C. Cordeiro, Eddie B. de Lima Filho
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…
Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)
Felipe R. M. Sousa, Lucas C. Cordeiro, Eddie B. de Lima Filho
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 elec…
Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking
Renato B. Abreu, Lucas Cordeiro, Eddie B. L. Filho
The implementation of digital filters in processors based on fixed-point arithmetic can lead to problems related to the finite word-length. In particular, the processing of signals…