TACO is a tool for formal verification of programs that helps developers find bugs in early stages. TACO translates annotated Java sources into DynAlloy in order to verify the generated specification using SAT solving as underlying formal method.

The aim of this presentation is to introduce TACO and two extensions developed as part of my MSc thesis. The first one, called “Back2Java”, generates automatically a Java witness of a detected bug. The second one implements a modular analysis on top of the DynAlloy code generator.

These extensions are intended to make the tool easier to use by hiding the underlying SAT solving from the user and also to contribute to the scalability of relational modeling, as the modular analysis can alleviate state explosion.

This is joint work with Nazareno Aguirre, Nicolás Ricci and Juan Galeotti.