Combining techniques of bounded model checking and constraint programming to aid for error localization

详细信息    查看全文

• 作者：Mohammed Bekkouche
• 关键词：Program verification ; Testing ; Debugging ; Error localization ; Constraint Programming ; LocFaults ; BugAssist ; Minimal correction subset ; Minimal correction deviation
• 刊名：Constraints
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：22
• 期：1
• 页码：93-94
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence (incl. Robotics); Optimization; Computing Methodologies; Operation Research/Decision Theory;
• 出版者：Springer US
• ISSN：1572-9354
• 卷排序：22

文摘

A model checker can produce a trace of counter-example for erroneous program, which is often difficult to exploit to locate errors in source code. In my thesis, we proposed an error localization algorithm from counter-examples, named LocFaults, combining approaches of Bounded Model-Checking (BMC) with constraint satisfaction problem (CSP). This algorithm analyzes the paths of CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of control flow graph for which at most k conditional statements can be wrong. Then we calculate the MCSs (Minimal Correction Sets) of limited size on each of these paths. Removal of one of these sets of constraints gives a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the postcondition. To calculate the MCSs, we extend the generic algorithm proposed by Liffiton and Sakallah in order to deal with programs with numerical instructions more efficiently. This approach has been experimentally evaluated on a set of academic and realistic programs.