activity
20202024
most citedIncremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors

4 citations · 7 across the 6 of their papers we have counts for

collaborators

6 papers

cs.CR2024

FuSeBMC AI: Acceleration of Hybrid Approach through Machine Learning

Kaled M. Alshmrany, Mohannad Aldughaim, Chenfeng Wei +3

We present FuSeBMC-AI, a test generation tool grounded in machine learning techniques. FuSeBMC-AI extracts various features from the program and employs support vector machine and…

cs.SE2022★ 1 cited

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…

cs.CR2021

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…

cs.CR2020★ 1 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.SE2020★ 4 cited

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…

cs.CR2020★ 1 cited

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…