Paper Info
Title
Practical JFSL verification using TACO
Abstract
AbstractTranslation 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.
Year
DOI
Venue
2014
10.1002/spe.2237
Periodicals
Keywords
DocType
Volume
static analysis,bounded verification,eclipse plug-in,TACO,test case generation
Journal
44
Issue
ISSN
Citations 
3
0038-0644
0
PageRank 
References 
Authors
0.34
15
3
Name
Order
Citations
PageRank
Marcos Chicote191.03
Daniel Ciolek2121.54
Juan Pablo Galeotti31479.54