| Autor: |
Konighofer, Robert, Bloem, Roderick |
| Zdroj: |
2011 Formal Methods in Computer-Aided Design (FMCAD); 1/ 1/2011, p91-100, 10p |
| Abstrakt: |
In this paper, we present a novel debugging method for imperative software, featuring both automatic error localization and correction. The input of our method is an incorrect program and a corresponding specification, which can be given in form of assertions or as a reference implementation. We use symbolic execution for program analysis. This allows for a wide range of different trade-offs between resource requirements and accuracy of results. Our error localization method rests upon model-based diagnosis and SMT-solving. Error correction is done using a template-based approach which ensures that the computed repairs are readable. Our method can handle all sorts of incorrect expressions, not only under a single-fault assumption but also for multiple faults. Finally, we present experimental results, where an implementation for C programs is used to debug mutants of the TCAS case study of the Siemens suite. [ABSTRACT FROM PUBLISHER] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
