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

TACO: Translation of Annotated COde


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


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 


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

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



  • 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)



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


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