LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software Projects

Janislley Oliveira de Sousa, Bruno Carvalho de Farias, Thales Araujo da Silva, Eddie Batista de Lima Filho, Lucas Carvalho Cordeiro

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


Researchers continue to advance the state-of-the-art of software vulnerability analysis. Software validation and verification techniques are indispensable tools for cultivating robust systems characterized by high levels of dependability and reliability. Remarkably, the pressing concern of memory errors in C software looms large in the landscape of systems security. This paper introduces the innovative tool called LSVerifier, leveraging the bounded model checking technique to effectively detect security vulnerabilities in C open-source software. The proposed tool emerges as a pivotal asset for identifying vulnerabilities and generating an output report summarizing the software weaknesses found. The method’s efficacy was validated through real-world applications. The results show that LSVerifier was able to check complex open-source software, identifying software issues that could potentially result in vulnerabilities.
Original languageEnglish
Title of host publicationXXIII Brazilian Symposium on Information and Computational Systems Security
Publication statusPublished - 18 Sept 2023


Dive into the research topics of 'LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software Projects'. Together they form a unique fingerprint.

Cite this