Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples
One of the main challenges in software development is to ensure the correctness and reliability of software systems. In this sense, a system failure or malfunction can result in a catastrophe especially in critical embedded systems. In the context of software verification, bounded model checkers (BMCs) have already been applied to discover subtle errors in real projects. When a model checker finds an error, it produces a counter-example. On one hand, the value of counter-examples to debug software systems is widely recognized in the state-of-the-practice. On the other hand, model checkers often produce counter-examples that are either too large or difficult to be understood mainly because of the software size and the values chosen by the respective solver. This paper proposes a method with the purpose of automating the collection and manipulation of counter-examples in order to generate new instantiated code to reproduce the identified error. The proposed method may be seen as a complementary technique for the verification performed by state-of-the-art BMC tools. In particular, we used the ESBMC model checker to show the effectiveness of the proposed method over publicly available benchmarks and, additionally, a comparison with the tool Frama-C.
KeywordsModel Checker Bound Model Check Property Violation Software Model Checker Automate Software Engineer
Unable to display preview. Download preview PDF.
- 1.Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)Google Scholar
- 2.Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. In: CEA LIST and INRIA (2009), http://frama-c.cea.fr/acsl.html
- 4.Canet, G., Cuoq, P., Monate, B.: A Value Analysis for C Programs. In: Intl. Conf. on Source Code Analysis and Manipulation (SCAM), pp. 123–124 (2009)Google Scholar
- 5.Cordeiro, L., Fischer, B.: Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking. In: Intl. Conf. on Software Engineering (ICSE), pp. 331–340 (2011)Google Scholar
- 6.Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Transactions on Software Engineering (TSE) 99 (2011), http://eprints.ecs.soton.ac.uk/22291/
- 9.Ji, J.H., Woo, G., Park, H.B., Park, J.S.: Design and Implementation of Retargetable Software Debugger Based on GDB. In: Intl. Conf. on Convergence and Hybrid Information Technology (CHIT), vol. 1, pp. 737–740 (2008)Google Scholar
- 10.Marché, C., Moy, Y.: Jessie plugin tutorial. In: INRIA (2010), http://frama-c.com/download/jessie-tutorial-Carbon-20101201-beta1.pdf
- 13.Taghdiri, M.: Inferring Specifications to Detect Errors in Code. In: Intl. Conf. on Automated Software Engineering (ASE), pp. 144–153 (2004)Google Scholar
- 14.Tip, F.: A survey of program slicing techniques. Journal Programming Languages 3(3) (1995)Google Scholar