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. © 2012 IEEE.
Registro:
| Documento: |
Conferencia
|
| Título: | TacoPlug: An eclipse plug-in for TACO |
| Autor: | Chicote, M.; Galeotti, J.P. |
| Ciudad: | Zurich |
| Filiación: | Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina
CONICET, Argentina
|
| Palabras clave: | bounded verification; Eclipse plug-in; Static analysis; TACO; Debuggers; Eclipse plugin; Plug-ins; Software errors; Source codes; TACO; Computer architecture; Static analysis; Program debugging |
| Año: | 2012
|
| Página de inicio: | 37
|
| Página de fin: | 42
|
| DOI: |
http://dx.doi.org/10.1109/TOPI.2012.6229808 |
| Título revista: | 2012 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012
|
| Título revista abreviado: | Int. Workshop Dev. Tools Plug-Ins, TOPI - Proc.
|
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97814673_v_n_p37_Chicote |
Referencias:
- Clarke, E., Kroening, D., Lerda, F., A Tool for Checking ANSI-C Programs LNCS, 2988, pp. 168-176. , TACAS 2004
- Cormen, T., Leiserson, C., Rivest, R., Stein, C., (2009) Introduction to Algorithms, , (3. ed.) MIT Press
- Dennis, G., (2009) A Relational Framework for Bounded Program Verification, , MIT PhD Thesis. July
- Dolby, J., Vaziri, M., Tip, F., Finding Bugs Efficiently with a SAT Solver (2007) ESEC/FSE'07, pp. 195-204. , ACM Press
- Een, N., Sorensson, N., An extensible SAT-solver (2004) LNCS, 2919, pp. 502-518
- Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N., DynAlloy: Upgrading Alloy with Actions (2005) ICSE'05, pp. 442-450
- Galeotti, J., Rosner, N., Lopez Pombo, C., Frias, M., Analysis of Invariants for Efficient Bounded Verification ISSTA 2010, Trento, Italy
- Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P., F-Soft: Software Verification Platform (2005) CAV'05, pp. 301-306
- Jackson, D., (2006) Software Abstractions, , MIT Press
- Leavens, G., Baker, A., Ruby, C., Preliminary design of JML: A behavioural interface specification language for Java (2006) ACM Software Engineering Notes, 31 (3). , May
- Müller, P., Ruskiewicz, J., Using Debuggers to Understand Failed Verification Attempts (2011) Formal Methods (FM) 2011, pp. 73-87
- Visser, W., Pǎsǎreanu, C.S., Pelánek, R., Test Input Generation for Java Containers using State Matching (2006) ISSTA 2006, pp. 37-48
- Xie, Y., Aiken, A., Saturn: A scalable framework for error detection using Boolean satisfiability (2007) ACM TOPLAS, 29 (3)
- Yessenov, K., (2009) A Light-weight Specification Language for Bounded Program Verification, , MIT MEng Thesis. May
- Zimmermann, T., Zeller, A., Visualizing Memory Graphs Software Visualization 2001, pp. 191-204
Citas:
---------- APA ----------
Chicote, M. & Galeotti, J.P.
(2012)
. TacoPlug: An eclipse plug-in for TACO. 2012 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012, 37-42.
http://dx.doi.org/10.1109/TOPI.2012.6229808---------- CHICAGO ----------
Chicote, M., Galeotti, J.P.
"TacoPlug: An eclipse plug-in for TACO"
. 2012 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012
(2012) : 37-42.
http://dx.doi.org/10.1109/TOPI.2012.6229808---------- MLA ----------
Chicote, M., Galeotti, J.P.
"TacoPlug: An eclipse plug-in for TACO"
. 2012 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012, 2012, pp. 37-42.
http://dx.doi.org/10.1109/TOPI.2012.6229808---------- VANCOUVER ----------
Chicote, M., Galeotti, J.P. TacoPlug: An eclipse plug-in for TACO. Int. Workshop Dev. Tools Plug-Ins, TOPI - Proc. 2012:37-42.
http://dx.doi.org/10.1109/TOPI.2012.6229808