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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Publicado: 2014
Materias:
bounded verification
eclipse plug-in
static analysis
TACO
test case generation
Bounded verifications
Formal tools
Java program
Plug-ins
Software errors
Source codes
Test case generation
Computer software
Java programming language
Program translators
Static analysis
Tools
Program debugging
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00380644_v44_n3_p317_Chicote
http://hdl.handle.net/20.500.12110/paper_00380644_v44_n3_p317_Chicote
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_00380644_v44_n3_p317_Chicote
record_format dspace
spelling paper:paper_00380644_v44_n3_p317_Chicote2023-06-08T15:02:26Z Practical JFSL verification using TACO 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. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00380644_v44_n3_p317_Chicote 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
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.
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
publishDate 2014
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00380644_v44_n3_p317_Chicote
http://hdl.handle.net/20.500.12110/paper_00380644_v44_n3_p317_Chicote
_version_ 1768542827513380864

Ejemplares similares