Herramientas Personales
Usted está aquí: Inicio Investigación Grupos de Investigación rfm taco

TACO: Translation of Annotated COde

taco_logo.gif

Welcome to TACO Homepage

About TACO

TACO is an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification. TACO uses a bounded verification technique, in which all executions of a procedure are examined up to a user-provided bound on the heap and number of loop unrollings. TACO translates Java annotated code to JDynAlloy (an intermediate language representation) which then is translated to DynAlloy.

Latest News

 

Installing TACO

1.Download taco.zip (version 1.01). It requires Java 1.6.

2. Unzip the archive

3.Run TACO:

java -jar taco.jar -cf {configfile} -c {classname} -m {methodname} 

The available architectures are: amd64-linux , x86-freebsd , x86-linux , x86-mac , x86-windows

The TACO source code can be downloaded from taco_src.jar (version 1.01)

Running TACO

Running a simple example

Execute: :

 

java -jar taco.jar -cf examples.properties -c SimpleCode -m inc

This analysis should give you a counterexample, because procedure "inc" ensures that the result is equals to 0, which is clearly not possible under the requirement that argument "x" requires to be equal to 1.

Execute :

java -jar taco.jar -cf examples.properties -c SimpleCode -m dec

On the other hand, procedure "dec" returns no counterexample since the specification is valid.

Running a more challenging example

Execute:

java -jar taco.jar -cf examples.properties -c BoundedStack -m pushBuggy


Since the pushBuggy method is not increasing the value of the size field, the ensures clause: size==\old(size)+1 is violated. This results in a counterexample 

Execute:

java -jar taco.jar -cf examples.properties -c BoundedStack -m push

Since the push method is fixed, TACO reports no counterexample.

Benchmarks

Publications

  • Juan Pablo Galeotti, Nicolas Rosner, Carlos Gustavo Lopez Pombo, Marcelo Frias. Analysis of Invariants for Efficient Bounded Verification. International Symposium on Software Testing and Analysis (ISSTA), Trento, Italy, July 2010. (PDF)

 

Contact

For any problem / question regarding TACO, please email to these addresses {jgaleotti, rfm} AT dc DOT uba DOT ar

Acknowledgments

TACO depends on the following open-source projects: Alloy, ANTLR, Apache ANT, Apache Commons, JUnit, Log4J, JML, MultiJava, JForge and KodKod

alloy.gifantlr.gifapache-ant.gifapache-commons.pngjunit.jpglog4j.jpgjml.jpg  multijava.jpg jforge.jpg  kodkod.jpg