Refinement of structural heuristics for model checking of concurrent programs through data mining

详细信息    查看全文

• 作者：Reed Milewicz ; ^{rmmilewi@cis.uab.edu} ; Peter Pirkelbauer ^{pirkelbauer@uab.edu}
• 关键词：Model checking ; Structural heuristics ; Data mining
• 刊名：Computer Languages, Systems & Structures
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：47
• 期：part_P2
• 页码：170-188
• 全文大小：1178 K
• 卷排序：47

文摘

The paper explores how model checking can be hybridized with trace analysis. Traces are mined to produce a categorical model of thread behavior. A heuristic for race detection is retrofitted to exploit the behavior model. With proper parameterization, the novel heuristic finds bugs 8× faster. A novel mutation-based benchmark generation process is introduced for validation.