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

• May 10 2010 : New TACO 1.01 is released. TACO accepts annotations written in JForge Specification Language (JFSL)  as well as annotations written in Java Modeling Language (JML).
  

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

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

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

• Java containers benchmark. The experimental data for the ISSTA 2010 article can be found here.
• KOA benchmark. The Remote Voting System developed for the Dutch government in 2003.
  

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