Localizing Program Errors for Cimple Debugging

Abstract. We present automated techniques for the explanation of counterexamples, where a counter-example should be understood as a sequence of program statements. Our approach is based on variable dependency analysis and is applicable to programs written in Cimple, an expressive subset of the C programming language. Central to our approach is the derivation of a focusstatement sequence (FSS) from a given counter-example: a subsequence of the counter-example containing only those program statements that directly or indirectly affect the variable valuation leading to the program error behind the counter-example. We develop a ranking procedure for FSSs where FSSs of higher rank are conceptually easier to understand and correct than those of lower rank. We also analyze constraints over uninitialized variables in order to localize program errors to specific program segments; this often allows the user to subsequently take appropriate debugging measures. We have implemented our techniques i...

• Type: Conference
• Year: 2004
• Where: FORTE
• Authors: Samik Basu, Diptikalyan Saha, Scott A. Smolka
• Keywords: FORTE 2004, FORTE 2007, Program Errors, Program Statements, Variable Dependency Analysis