TacoPlug: An Eclipse plug-in for TACO

Author

Chicote, Marcos ; Galeotti, Juan Pablo

Author_Institution

Dept. de Comput., FCEyN, Buenos Aires, Argentina

fYear

2012

fDate

3-3 June 2012

Firstpage

37

Lastpage

42

Abstract

In this work we present TacoPlug, an Eclipse plugin 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

formal specification; program debugging; program diagnostics; program verification; Eclipse plugin; TACO bounded verifier; TacoPlug interface; annotated software verification; annotated source code; bounded verification; debugging experience; error traces output; fault understanding; real-life software error; software debugger; static analysis; Data structures; Debugging; Feature extraction; Java; Navigation; Usability; Eclipse plug-in; Static analysis; TACO; bounded verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Developing Tools as Plug-ins (TOPI), 2012 2nd Workshop on

Conference_Location

Zurich

Print_ISBN

978-1-4673-1819-8

Type

conf

DOI

10.1109/TOPI.2012.6229808

Filename

6229808