TacoPlug: An Eclipse Plug-In for TACO

Abstract—In this work we present TacoPlug, an Eclipse plug-in that lets users explore error traces output by the bounded verifier TACO. TacoPlug uses and extends TACO to provide a better debugging experience. TacoPlug interface allows the user to verify an annotated software using the TACO verifier. If TACO finds a violation to the specification, TacoPlug presents it in terms of the annotated source code. TacoPlug features several views of the error trace to facilitate fault understanding. It resembles any software debugger, but the debugging occurs statically without executing the program. We show the usability of our tool by means of a motivational example taken from a real-life software error. Keywords-Static analysis, bounded verification, Eclipse plug-in, TACO. I