A sumary of "Bandera: Extracting Finite-state Models from Java Source Code" by Corbett, Dwyer, Hatcliff, Laubach, Pasareanu, Robby, Zheng summary by Steve Haga Bandera is a tool for program verification using finite-state methods. This is a daunting task, which Bandera accomplises in several steps, leveraging much prior work. The goal of Bandera is to present an easy to use interface to the user, so that the people will actually use the tool. In fact, my initial interest to choose this paper for review was that I was interested in seeing how the theoretical techniques described in class might translate into a practical implementation, that I might want to use in the future for my debugging. Bandera can alert the user if his code does not perform as he believes it should. The user can view his code in a graphical interface. At any point, he can assert some proposition that he believes to be true, such as "if the queue becomes non-empty, the stage will terminate." Care is taken to make the specification of a proposition as simple as possible. Once a propsition is given, Bandera employs Finite State Verification to see if there aare any counter examples. If Bandera finds an execution path that violates the proposition, it will show the user, in his java code, the sequence of executed lines that leads to the violation. If such a tool can perform its evaluation in a reasonable time, Bandera seams to offer real promise of wide use. Finite-State Verification methods are hard to apply to software, although they have been used successfully to verify some critical hardware systems. Three obstacles to applying these methods to software. First, programs, unlike hardware, may not contain a finite state. Constructs such as recursion allow for an unbouded heap, an unbounded number of function calls, and many other other unbounded behaviors. Sometimes, even in the presence of recursion, a bound on the depth of recursion can be determined. In other cases, the only solution is to approximate program behavior by arbitrarily limttimg recursion to a certain depth. In this way, an approximate, finite state model can be created. The second obstacle is that Finite-State Verification is time consuming. To address this, Bandera agressively reduces the size of the state machine, using techniques known as slicing, data abstraction, and component restriction. These are discussed below. The third obstacle is that Finite-State Verification software has required significant effort from the user. For instance, to specify a simple proposition like "between the time an elevator is called and the time the doors open, the elevator can only arrive at the floor at most 2 times," requires a very complicated and error-prone specification in existing techniques (as described in their reference #7). This obstacle is overcome by using some of their prior work (reference #7), to isolate common patterns in the propositions, which are there called property specifications. Since most specifications fall into a common set of patterns, these patterns can be remembered, rather than requiring the user to retype them each time. In this way, users who are not experts in Finite-State Verification languages can still use Bandera to test their programs. Bandera is implemented in eight steps. First, Bandera allows the user to specify his proposition. As mention breifly in the last paragraph, and as discussed extensively in their prior work, patterns are more user friendly than previous techniques. Second, Bandera uses the Soot compiler to create an intermediate representaition of Java, called Jimple. Soot was modified to maintain more information about the program lines that correspond to Jimple lines. This becomes necesary when optimizations choose to inline functions, among other causes. Bandera requires this extra information, because it needs to be able to show the user the sequence of original Java instructions that leads to the conflict. Third, Bandera performs slicing. Before the Jimple code is converted to the form required by an existing Finite-State verifier, Bandera must reduce the code size, so that the Finite State veirifer can accomplish its work in a reasonable time. The first reduction is slicing. Slicing is a form of partial evaluation. Only those portions of code that directly affect the given proposition are considered. The rest is pruned away, and will be shown in a faded font by the Bandera GUI. Slicing methods are well understood. In particular, Horowitz applied slicing across procedures (reference #17 in the paper). Slicing techniques are complex, but invisible to the user of Bandera, which performs slicing automatically. Slicing involves the construction of a novel dependence graph, and the subsequent removal of those nodes which contain no path to the proposed condition. The amount of code which can be pruned away varies according to the proposition, but was shown in the results to markedly reduce the verification time (from 2674 sec to 4 sec). Fourth, Bandera aplies data abstraction. Bandera contains a library of possible abstractions, such as the sign of a number, or its modulo value (useful for identifying even/odd relationships). Abstraction methods were shown to further reduce the verification time, but not as markedly. Abstraction also has the negative effect of introduces further approximations, with the potential of identifying false counter-examples, for impossible paths. Fifth Bandera may apply component restriction. If the verifier takes too long, the user may restrict components, such as by limiting the rangews of variables. Component restriction is also necessary to bound recursive behaiors. Sixth, the Bandera back end generates code in the form required by a given finite-state verifier. This is innovation allows bandera not to be tied to a particular verifier. As better verifiers are designed, only the back-end of Bandera must be retargetted. In the paper, Bandera is tested with SPIN. Seventh, the verifier is run. Eigth, if there is a conflict, the GUI will display the steps of the counter-example in terms of the original Java code. This is an important feature, because the output of the verifiers is otherwise hard to interpret. In their example, they identify a 159 statement long counter-example. This corresponds to 1780 steps in the verifier, which is much longer and more complex. Although the results are not thorough, the technique seems very promising.