We are happy to announce that the following two tool papers have been accepted for publication at the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13) that will take place in Hanoi, Vietnam, on 15-18 October 2013. * LTL Model Checking with Neco - Łukasz Fronc (IBISC, Université d'Évry/Paris-Saclay) - Alexandre Duret-Lutz (LRDE, EPITA) We introduce neco-spot, an LTL model checker for Petri net models. It builds upon Neco, a compiler turning Petri nets into native shared libraries that allows fast on-the-fly exploration of the state-space, and upon Spot, a C++ library of model-checking algorithms. We show the architecture of Neco and explain how it was combined with Spot to build an LTL model checker. http://publis.lrde.epita.fr/201310-ATVAb * Manipulating LTL formulas using Spot 1.0 - Alexandre Duret-Lutz (LRDE, EPITA) We present a collection of command-line tools designed to generate, filter, convert, simplify, lists of Linear-time Temporal Logic formulas. These tools were introduced in the release 1.0 of Spot, and we believe they should be of interest to anybody who has to manipulate LTL formulas. We focus on two tools in particular: ltlfilt, to filter and transform formulas, and ltlcross to cross-check LTL-to-Büchi-Automata translators. http://publis.lrde.epita.fr/201310-ATVAa -- Alexandre Duret-Lutz