TacoPlug: An eclipse plug-in for TACO
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 f...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2012
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 04838caa a22006497a 4500 | ||
|---|---|---|---|
| 001 | PAPER-9464 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203923.0 | ||
| 008 | 190411s2012 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-84864265939 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Chicote, M. | |
| 245 | 1 | 0 | |a TacoPlug: An eclipse plug-in for TACO |
| 260 | |c 2012 | ||
| 270 | 1 | 0 | |m Chicote, M.; Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina; email: mchicote@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Clarke, E., Kroening, D., Lerda, F., A Tool for Checking ANSI-C Programs LNCS, 2988, pp. 168-176. , TACAS 2004 | ||
| 504 | |a Cormen, T., Leiserson, C., Rivest, R., Stein, C., (2009) Introduction to Algorithms, , (3. ed.) MIT Press | ||
| 504 | |a Dennis, G., (2009) A Relational Framework for Bounded Program Verification, , MIT PhD Thesis. July | ||
| 504 | |a Dolby, J., Vaziri, M., Tip, F., Finding Bugs Efficiently with a SAT Solver (2007) ESEC/FSE'07, pp. 195-204. , ACM Press | ||
| 504 | |a Een, N., Sorensson, N., An extensible SAT-solver (2004) LNCS, 2919, pp. 502-518 | ||
| 504 | |a Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N., DynAlloy: Upgrading Alloy with Actions (2005) ICSE'05, pp. 442-450 | ||
| 504 | |a Galeotti, J., Rosner, N., Lopez Pombo, C., Frias, M., Analysis of Invariants for Efficient Bounded Verification ISSTA 2010, Trento, Italy | ||
| 504 | |a 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 | ||
| 504 | |a Jackson, D., (2006) Software Abstractions, , MIT Press | ||
| 504 | |a 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 | ||
| 504 | |a Müller, P., Ruskiewicz, J., Using Debuggers to Understand Failed Verification Attempts (2011) Formal Methods (FM) 2011, pp. 73-87 | ||
| 504 | |a 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 | ||
| 504 | |a Xie, Y., Aiken, A., Saturn: A scalable framework for error detection using Boolean satisfiability (2007) ACM TOPLAS, 29 (3) | ||
| 504 | |a Yessenov, K., (2009) A Light-weight Specification Language for Bounded Program Verification, , MIT MEng Thesis. May | ||
| 504 | |a Zimmermann, T., Zeller, A., Visualizing Memory Graphs Software Visualization 2001, pp. 191-204 | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina | ||
| 593 | |a CONICET, Argentina | ||
| 690 | 1 | 0 | |a BOUNDED VERIFICATION |
| 690 | 1 | 0 | |a ECLIPSE PLUG-IN |
| 690 | 1 | 0 | |a STATIC ANALYSIS |
| 690 | 1 | 0 | |a TACO |
| 690 | 1 | 0 | |a DEBUGGERS |
| 690 | 1 | 0 | |a ECLIPSE PLUGIN |
| 690 | 1 | 0 | |a PLUG-INS |
| 690 | 1 | 0 | |a SOFTWARE ERRORS |
| 690 | 1 | 0 | |a SOURCE CODES |
| 690 | 1 | 0 | |a TACO |
| 690 | 1 | 0 | |a COMPUTER ARCHITECTURE |
| 690 | 1 | 0 | |a STATIC ANALYSIS |
| 690 | 1 | 0 | |a PROGRAM DEBUGGING |
| 700 | 1 | |a Galeotti, J.P. | |
| 711 | 2 | |c Zurich |d 3 June 2012 through 3 June 2012 |g Código de la conferencia: 91298 | |
| 773 | 0 | |d 2012 |h pp. 37-42 |p Int. Workshop Dev. Tools Plug-Ins, TOPI - Proc. |n 2012 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012 - Proceedings |z 9781467318204 |t 2012 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84864265939&doi=10.1109%2fTOPI.2012.6229808&partnerID=40&md5=8121a2b24d2acba490bc1432844308e8 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1109/TOPI.2012.6229808 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_97814673_v_n_p37_Chicote |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97814673_v_n_p37_Chicote |y Registro en la Biblioteca Digital |
| 961 | |a paper_97814673_v_n_p37_Chicote |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 70417 | ||