Explaining Inconclusive Outcomes from Software Model Checkers to Users
7This talk will be centered on partial verification results. Software model checkers can be used both to find bugs and to prove certain properties hold. However, due to resource bounds or tool limitations, many times neither is achieved. I will start by motivating this line of work and sharing my vision of how partial verification results can be explained to users (perhaps in an IDE) to provide meaningful feedback about the verification progress. I will briefly explain background on Abstract Reachability Trees, which we used to instantiate our techniques, and discuss their relevance along with related work. Subsequently, I will present two approaches to explaining partial software model checking results: model checking execution reports and coverage of partial software model checks. For model checking execution reports, I will illustrate how non-trivial insights about the thoroughness of the exploration can be extracted from inconclusive runs and discuss our preliminary evaluation results. For coverage of partial software model checks, I will explain some of the challenges we worked around to provide such a measure and analyze performance considerations. I will end the talk by discussing my broader research vision and how the topics of the talk fit into such a vision. This is joint work with Victor Braberman, Diego Garbervetsky and Sebastian Uchitel.
See more on this video at https://www.microsoft.com/en-us/research/video/explaining-inconclusive-outcomes-from-software-model-checkers-to-users/