Requirements Verification Through the Analysis of Source Code by Large Language Models

In the most recent years, Large Language Models (LLMs) have gained popularity and have been accepted and used in different domains due to their ability to understand and generate written language. LLMs allow us to analyze large amounts of data in a few moments, yet they are also extremely simple to use, making them a very powerful assistive tool that can aid in a wide range of tasks; from planning a family trip, to aid during the development process of a huge system. For software developers, LLMs have been mostly used for code generation, explanation, or optimization. Software verification is a crucial part of software development as it is the process of ensuring that a system meets specific requirements. Requirements specifications play a pivotal role in software verification as they define what a system should do. In this paper we propose the use of LLMs for code verification through the analysis of requirements specifications. We prove that LLMs, such as GPT-3.5, can verify a list of requirements through a given code and evaluate why the requirements have or have not been met.