Practical JFSL verification using TACO
by Marcos Chicote, Daniel Ciolek, Juan Pablo Galeotti

Journal of Software: Practice and Experience, Pages 317-334, Volume 44, Number 3, March 2014.

Digital Library via DOI: 10.1002/spe.2237 - Local copy: Download as PDF file.


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.


BibTeX Entry

    title = "Practical JFSL verification using TACO",
    author = "Marcos Chicote and Daniel Ciolek and Juan Pablo Galeotti",
    year = "2014",
    month = mar,
    journal = "Journal of Software: Practice and Experience",
    number = "3",
    pages = "317--334",
    volume = "44",
    doi = "10.1002/spe.2237",

Show all publications of the Software Engineering Chair.