Abstrakt. Även om motexempelet som returneras av en modellkontroll kan hjälpa till att återge symtom relaterade till en defekt, krävs det ofta en betydande ansträngning för programmeraren att tolka det för att lokalisera orsaken. I detta dokument tillhandahåller vi ett automatiserat förfarande för att zooma in till potentiella programvarudefekter genom att analysera ett enda konkret motexempel. Vår analys bygger på att man från motexempelet tar fram ett syntaktiskt bevis på ogenomförbarhet, d.v.s. en minimal uppsättning predikat på ordnivå som motsäger varandra. Förfarandet använder en effektiv, svagaste algoritm som utförs på en enda konkret genomförandebana, som är betydligt mer skalbar än andra modellkontrollbaserade metoder. Till skillnad från de flesta av de befintliga metoderna, behöver vi inte ytterligare exekvering spår annat än buggy en. Vi använder offentliga-domäner exempel för att visa effektiviteten i vår nya algoritm.
Till skillnad från det tidigare arbetet som kräver flera utföranden införde arbetet REF en teknik som utfördes på en enda betongutförandebana med hjälp av den svagaste förkonditionsalgoritmen.
Whodunit? Causal analysis for counterexamples
{'venue': 'In International Symposium on Automated Technology for Verification and Analysis (ATVA’06), volume 4218 of LNCS', 'journal': None, 'mag_field_of_study': ['Computer Science']}