Portal de Periódicos da CAPES

Capítulo de livro Produção Nacional Revisado por pares

BIBTEX RIS

Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples

2012; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-30729-4_10

1611-3349

Herbert Rocha, Raimundo Barreto, Lucas C. Cordeiro, Arilo Dias Neto,

Software Reliability and Analysis Research

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.