57 citations · 144 across the 48 of their papers we have counts for
53 papers
ESBMC v7.3: Model Checking C++ Programs using Clang AST
Kunjian Song, Mikhail R. Gadelha, Franz Brauße +2
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new clang-based C++ front-end. While the previous C…
A Privacy-Preserving and Accountable Billing Protocol for Peer-to-Peer Energy Trading Markets
Kamil Erdayandi, Lucas C. Cordeiro, Mustafa A. Mustafa
This paper proposes a privacy-preserving and accountable billing (PA-Bill) protocol for trading in peer-to-peer energy markets, addressing situations where there may be discrepanci…
The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification
Norbert Tihanyi, Tamas Bisztray, Ridhi Jain +3
This paper presents the FormAI dataset, a large collection of 112, 000 AI-generated compilable and independent C programs with vulnerability classification. We introduce a dynamic…
A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
Norbert Tihanyi, Ridhi Jain, Yiannis Charalambous +3
This paper introduces an innovative approach that combines Large Language Models (LLMs) with Formal Verification strategies for automatic software vulnerability repair. Initially,…
JBMC: A Bounded Model Checking Tool for Java Bytecode
Romain Brenguier, Lucas Cordeiro, Daniel Kroening +1
JBMC is an open-source SAT- and SMT-based bounded model checking tool for verifying Java bytecode. JBMC relies on an operational model of the Java libraries, which conservatively a…
LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)
Tong Wu, Edoardo Manino, Fatimah Aljaafari +2
We describe and evaluate LF-checker, a metaverifier tool based on machine learning. It extracts multiple features of the program under test and predicts the optimal configuration (…
ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation
Rafael Menezes, Daniel Moura, Helena Cavalcante +2
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 bu…
CEG4N: Counter-Example Guided Neural Network Quantization Refinement
João Batista P. Matos, Iury Bessa, Edoardo Manino +2
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 ch…
FuSeBMC v4: Improving code coverage with smart seeds via BMC, fuzzing and static analysis
Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat +1
Bounded model checking (BMC) and fuzzing techniques are among the most effective methods for detecting errors and security vulnerabilities in software. However, there are still sho…
Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
Fatimah K. Aljaafari, Rafael Menezes, Edoardo Manino +3
Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially wit…
FuSeBMC v.4: Smart Seed Generation for Hybrid Fuzzing
Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat +1
FuSeBMC is a test generator for finding security vulnerabilities in C programs. In earlier work [4], we described a previous version that incrementally injected labels to guide Bou…
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…
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…
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…
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…
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…
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…
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…
Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors
Mohannad Aldughaim, Kaled Alshmrany, Rafael Menezes +2
Bounded model checking (BMC) is vital for finding program property violations. For unsafe programs, BMC can quickly find an execution path from an initial state to the violated sta…
Generating Adversarial Inputs Using A Black-box Differential Technique
João Batista Pereira Matos Juúnior, Lucas Carvalho Cordeiro, Marcelo d'Amorim +1
Neural Networks (NNs) are known to be vulnerable to adversarial attacks. A malicious agent initiates these attacks by perturbing an input into another one such that the two inputs…
An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
Mikhail R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole
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 float…
Verifying Software Vulnerabilities in IoT Cryptographic Protocols
Fatimah Aljaafari, Lucas C. Cordeiro, Mustafa A. Mustafa
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…
Finding Security Vulnerabilities in Network Protocol Implementations
Kaled Alshmrany, Lucas Cordeiro
Implementations of network protocols are often prone to vulnerabilities caused by developers' mistakes when accessing memory regions and dealing with arithmetic operations. Finding…