Practical JFSL verification using TACO
Translation of Annotated COde (TACO) is a SAT-based tool for bounded verification of Java programs. One challenge many formal tools share is to provide a practical interface for a non-proficient user. In this article, we present an Eclipse plug-in for the static verifier TACO. This plug-in allows a...
Guardado en:
Autores principales: | , , |
---|---|
Formato: | JOUR |
Materias: | |
Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_00380644_v44_n3_p317_Chicote |
Aporte de: |
id |
todo:paper_00380644_v44_n3_p317_Chicote |
---|---|
record_format |
dspace |
spelling |
todo:paper_00380644_v44_n3_p317_Chicote2023-10-03T14:48:17Z Practical JFSL verification using TACO Chicote, M. Ciolek, D. Galeotti, J.P. bounded verification eclipse plug-in static analysis TACO test case generation Bounded verifications Formal tools Java program Plug-ins Software errors Source codes TACO Test case generation Computer software Java programming language Program translators Static analysis Tools Program debugging Translation of Annotated COde (TACO) is a SAT-based tool for bounded verification of Java programs. One challenge many formal tools share is to provide a practical interface for a non-proficient user. In this article, we present an Eclipse plug-in for the static verifier TACO. This plug-in allows a user to walk a counterexample trace mimicking a debugging session. TacoPlug (our plug-in) 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. Furthermore, should a dynamic analysis be required, TacoPlug presents the user with a unit test case generated by TACO based on the detected violation. We show the usability of our tool by means of a motivational example taken from a real-life software error. Copyright © 2013 John Wiley & Sons, Ltd. Copyright © 2013 John Wiley & Sons, Ltd. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00380644_v44_n3_p317_Chicote |
institution |
Universidad de Buenos Aires |
institution_str |
I-28 |
repository_str |
R-134 |
collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
topic |
bounded verification eclipse plug-in static analysis TACO test case generation Bounded verifications Formal tools Java program Plug-ins Software errors Source codes TACO Test case generation Computer software Java programming language Program translators Static analysis Tools Program debugging |
spellingShingle |
bounded verification eclipse plug-in static analysis TACO test case generation Bounded verifications Formal tools Java program Plug-ins Software errors Source codes TACO Test case generation Computer software Java programming language Program translators Static analysis Tools Program debugging Chicote, M. Ciolek, D. Galeotti, J.P. Practical JFSL verification using TACO |
topic_facet |
bounded verification eclipse plug-in static analysis TACO test case generation Bounded verifications Formal tools Java program Plug-ins Software errors Source codes TACO Test case generation Computer software Java programming language Program translators Static analysis Tools Program debugging |
description |
Translation of Annotated COde (TACO) is a SAT-based tool for bounded verification of Java programs. One challenge many formal tools share is to provide a practical interface for a non-proficient user. In this article, we present an Eclipse plug-in for the static verifier TACO. This plug-in allows a user to walk a counterexample trace mimicking a debugging session. TacoPlug (our plug-in) 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. Furthermore, should a dynamic analysis be required, TacoPlug presents the user with a unit test case generated by TACO based on the detected violation. We show the usability of our tool by means of a motivational example taken from a real-life software error. Copyright © 2013 John Wiley & Sons, Ltd. Copyright © 2013 John Wiley & Sons, Ltd. |
format |
JOUR |
author |
Chicote, M. Ciolek, D. Galeotti, J.P. |
author_facet |
Chicote, M. Ciolek, D. Galeotti, J.P. |
author_sort |
Chicote, M. |
title |
Practical JFSL verification using TACO |
title_short |
Practical JFSL verification using TACO |
title_full |
Practical JFSL verification using TACO |
title_fullStr |
Practical JFSL verification using TACO |
title_full_unstemmed |
Practical JFSL verification using TACO |
title_sort |
practical jfsl verification using taco |
url |
http://hdl.handle.net/20.500.12110/paper_00380644_v44_n3_p317_Chicote |
work_keys_str_mv |
AT chicotem practicaljfslverificationusingtaco AT ciolekd practicaljfslverificationusingtaco AT galeottijp practicaljfslverificationusingtaco |
_version_ |
1782026495207669760 |