Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an approach struggles to scale up and verify extensive code bases. Consequently, we have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker. In particular, we pre-process input source-code files and guide the respective model checker to explore them systematically. Moreover, the proposed scheme includes a function-wise prioritization strategy, which readily provides results for code entities according to a scale of importance. Experimental results using a real implementation of the proposed methodology show that it can efficiently verify large software systems. Besides, it presented low peak memory allocation when executed. We have evaluated our approach by verifying twelve popular open-source C projects, where we have found real software vulnerabilities that their developers confirmed.

翻译：基于计算机的系统已解决包括工业、军事、教育及可穿戴设备在内的多个领域问题。然而，此类系统需要高质量的软件来保障安全性与可靠性，这两点是现代软件产品的必备属性。我们认为有界模型检测技术能够有效检测通用软件系统中的漏洞，但该方法在扩展及验证大规模代码库时存在困难。为此，我们开发并评估了一种利用先进有界模型检测工具验证大型软件系统的方法。具体而言，我们对输入源代码文件进行预处理，引导相应的模型检测器对其进行系统性探索。此外，所提出的方案包含基于函数优先级的排序策略，能够根据重要程度快速提供代码实体的检测结果。基于该方法真实实现的实验结果表明，其能够高效验证大型软件系统，且运行过程中内存峰值分配较低。我们通过验证十二个流行的开源C项目对该方法进行了评估，实际发现了经开发者确认的软件漏洞。