paper-with-me

Papers

Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview

2025-03-13 · Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Bilel Cherif, Richard A. Dubniczky, Ridhi Jain, Lucas C. Cordeiro

Software testing and verification are critical for ensuring the reliability and security of modern software systems. Traditionally, formal verification techniques, such as model checking and theorem proving, have provided rigorous frameworks for detecting bugs and vulnerabilities. However, these methods often face scalability challenges when applied to complex, real-world programs. Recently, the advent of Large Language Models (LLMs) has introduced a new paradigm for software analysis, leveraging their ability to understand insecure coding practices. Although LLMs demonstrate promising capabilities in tasks such as bug prediction and invariant generation, they lack the formal guarantees of classical methods. This paper presents a comprehensive study of state-of-the-art software testing and verification, focusing on three key approaches: classical formal methods, LLM-based analysis, and emerging hybrid techniques, which combine their strengths. We explore each approach's strengths, limitations, and practical applications, highlighting the potential of hybrid systems to address the weaknesses of standalone methods. We analyze whether integrating formal rigor with LLM-driven insights can enhance the effectiveness and scalability of software verification, exploring their viability as a pathway toward more robust and adaptive testing frameworks.

📄 PDF Abstract BibTeX arXiv:2503.10784

Code (0)

등록된 구현이 없습니다.

Tasks

Automated Theorem Provingsoftware testingVulnerability Detection

Similar Papers 제목 키워드 기반

LLMs as verification oracles for Solidity

2025-09-23 · Massimo Bartoletti, Enrico Lipparini, Livio Pompianu arxiv

Ensuring the correctness of smart contracts is critical, as even subtle flaws can lead to severe financial losses. While bug detection tools able to spot common vulnerability patterns can serve as a first line of defense…

Vulnerability Detection

CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection

2024-11-20 · Cristian Curaba, Denis D'Ambrosi, Alessandro Minisini, Natalia Pérez-Campanero Antolín

Cryptographic protocols play a fundamental role in securing modern digital infrastructure, but they are often deployed without prior formal verification. This could lead to the adoption of distributed systems vulnerable …

Vulnerability Detection

ParaVul: A Parallel Large Language Model and Retrieval-Augmented Framework for Smart Contract Vulnerability Detection

2025-10-20 · Tenghui Huang, Jinbo Wen, Jiawen Kang, Siyong Chen 외 arxiv

Smart contracts play a significant role in automating blockchain services. Nevertheless, vulnerabilities in smart contracts pose serious threats to blockchain security. Currently, traditional detection methods primarily …

Vulnerability Detection

Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models

2025-09-16 · Ştefan-Claudiu Susan, Andrei Arusoaie, Dorel Lucanu arxiv

The high rate of false alarms from static analysis tools and Large Language Models (LLMs) complicates vulnerability detection in Solidity Smart Contracts, demanding methods that can formally or empirically prove the pres…

Vulnerability Detection

A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification

2023-05-24 · Norbert Tihanyi, Ridhi Jain, Yiannis Charalambous, Mohamed Amine Ferrag 외

This paper introduces an innovative approach that combines Large Language Models (LLMs) with Formal Verification strategies for automatic software vulnerability repair. Initially, we employ Bounded Model Checking (BMC) t…

C++ codeMathematical Proofs