The rapid expansion of the Internet of Things (IoT) has made software security and reliability a critical concern. With multi-language programs running on edge computing, embedded systems, and sensors, each connected device represents a potential attack vector, threatening data integrity and privacy. Symbolic execution is a key technique for automated vulnerability detection. However, unknown function interfaces, such as sensor interactions, limit traditional concrete or concolic execution due to uncertain function returns and missing symbolic expressions. Compared with system simulation, the traditional method is to construct an interface abstraction layer for the symbolic execution engine to reduce the cost of simulation. Nevertheless, the disadvantage of this solution is that the manual modeling of these functions is very inefficient and requires professional developers to spend hundreds of hours. In order to improve efficiency, we propose an LLM-based automated approach for modeling unknown functions. By fine-tuning a 20-billion-parameter language model, it automatically generates function models based on annotations and function names. Our method improves symbolic execution efficiency, reducing reliance on manual modeling, which is a limitation of existing frameworks like KLEE. Experimental results primarily focus on comparing the usability, accuracy, and efficiency of LLM-generated models with human-written ones. Our approach was integrated into one verification platform project and applied to the verification of smart contracts with distributed edge computing characteristics. The application of this method directly reduces the manual modeling effort from a month to just a few minutes. This provides a foundational validation of our method’s feasibility, particularly in reducing modeling time while maintaining quality. This work is the first to integrate LLMs into formal verification, offering a scalable and automated verification solution for sensor-driven software, blockchain smart contracts, and WebAssembly systems, expanding the scope of secure IoT development.

Integrating Natural Language Processing (NLP) with Generative Pre-trained Transformer (GPT) models plays a pivotal role in enhancing the accuracy and efficiency of healthcare software, which is essential for patient safety and providing high-quality care. The precision of healthcare software is fundamental to protecting the well-being of the patient. In addition, it can ensure the delivery of superior care, maintain the integrity of healthcare systems, and promote trust and cost-effectiveness. It is necessary to emphasize the importance of software reliability in its development and deployment. Symbolic execution serves as a vital technology in automated vulnerability detection. However, symbolic execution often faces problems such as path explosion, which seriously affects efficiency. Although there have been several studies to reduce the number of computational paths in symbolic execution, this problem remains a major obstacle. Therefore, more efficient solutions are urgently needed to ensure the software security. This paper proposes a large-scale language model(LLM) induction method mitigating path explosion applied to symbolic execution engines. In contrast to traditional symbolic execution engines, which often result in timeout or out-of-memory detection, our approach achieves the task of detecting vulnerabilities in seconds. Furthermore, our proposal improves the scalability of symbolic execution, allowing more extensive and complex programs to be analyzed without significant increases in computational resources or time. This scalability is crucial to tackling modern software systems and improving the efficiency and effectiveness of automated defect verification in healthcare software.