The Path Explorer. The Path Inspector either proves that an assertion query is true, or provides a counter example execution path, which is displayed in the Path Explorer window (above). When multiple counter examples are possible, it presents a list of counter examples to the user; the user can select one to investigate more closely. Here, the Path Explorer is displaying a counterexample to an assertion query. The user can step through the counter example, much like stepping with a traditional debugger. (However, CodeSurfer’s analysis is all done statically, without running the code.) The code that corresponds to the selected statement is automatically highlighted in the CodeSurfer File Viewer. Using the Elision menu in the Path Explorer, it is possible to hide program points that are less relevant to the results. A set of elided points is shown as “…”. This gives the user a both a high-level view of the counter example and the ability to drill down to see the details.