research
∙
09/07/2023
NeuroCodeBench: a plain C neural network benchmark for software verification
Safety-critical systems with neural network components require strong gu...
share
research
∙
08/10/2023
ESBMC v7.3: Model Checking C++ Programs using Clang AST
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context...
research
∙
07/13/2023
SecureFalcon: The Next Cyber Reasoning System for Cyber Security
Software vulnerabilities leading to various detriments such as crashes, ...
research
∙
07/10/2023
A Privacy-Preserving and Accountable Billing Protocol for Peer-to-Peer Energy Trading Markets
This paper proposes a privacy-preserving and accountable billing (PA-Bil...
research
∙
07/05/2023
The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification
This paper presents the FormAI dataset, a large collection of 112, 000 A...
research
∙
06/25/2023
Revolutionizing Cyber Threat Detection with Large Language Models
Natural Language Processing (NLP) domain is experiencing a revolution du...
research
∙
06/23/2023
QNNRepair: Quantized Neural Network Repair
We present QNNRepair, the first method in the literature for repairing q...
research
∙
05/24/2023
A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
In this paper we present a novel solution that combines the capabilities...
research
∙
01/22/2023
LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)
We describe and evaluate LF-checker, a metaverifier tool based on machin...
research
∙
07/09/2022
CEG4N: Counter-Example Guided Neural Network Quantization Refinement
Neural networks are essential components of learning-based software syst...
research
∙
06/28/2022
FuSeBMC v4: Improving code coverage with smart seeds via fuzzing and static analysis
Bounded model checking (BMC) and fuzzing techniques are among the most e...
research
∙
06/13/2022
Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
Finding software vulnerabilities in concurrent programs is a challenging...
research
∙
06/09/2022
ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation
In this work, we describe and evaluate the first model checker for verif...
research
∙
12/20/2021
FuSeBMC v.4: Smart Seed Generation for Hybrid Fuzzing
FuSeBMC is a test generator for finding security vulnerabilities in C pr...
research
∙
11/25/2021
ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts
Smart contracts written in Solidity are programs used in blockchain netw...
research
∙
07/02/2021
Model Checking C++ Programs
In the last three decades, memory safety issues in system programming la...
research
∙
03/21/2021
EBF: A Hybrid Verification Tool for Finding Software Vulnerabilities in IoT Cryptographic Protocols
Internet of Things (IoT) consists of a large number of smart devices con...
research
∙
12/21/2020
FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs
We describe and evaluate a novel white-box fuzzer for C programs named F...
research
∙
04/27/2020
An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
We describe a new SMT bit-blasting API for floating-points and evaluate ...
research
∙
01/27/2020
Verifying Software Vulnerabilities in IoT Cryptographic Protocols
Internet of Things (IoT) is a system that consists of a large number of ...
research
∙
07/30/2019
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA
Artificial Neural networks (ANNs) are powerful computing systems employe...
research
∙
06/27/2019
Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification
The proliferation of Unmanned Aerial Vehicles (UAVs) embedded with vulne...
research
∙
04/12/2019
Boost the Impact of Continuous Formal Verification in Industry
Software model checking has experienced significant progress in the last...
research
∙
04/04/2019
Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space
We describe and evaluate a novel k-induction proof rule called bidirecti...
research
∙
10/29/2018
SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer
We describe and evaluate a bug refutation extension for the Clang Static...
research
∙
08/14/2017
Counterexample Guided Inductive Optimization Applied to Mobile Robots Path Planning (Extended Version)
We describe and evaluate a novel optimization-based off-line path planni...
research
∙
06/07/2017
Counterexample-Guided k-Induction Verification for Fast Bug Detection
Recently, the k-induction algorithm has proven to be a successful approa...
research
∙
04/11/2017