Fitzroy - A CTL*(FO) model checker

Fitzroy is a model-checker for the logic CTL* over fragments of first-order logic. Unlike most other systems, it supports modelling of states with a rich structure using lists, arrays and records and first-order logic.

Paper

Martin Diller Andreas Bauer, Peter Baumgartner and Michael Norrish.
Tableaux for Verification of Data-Centric Processes.
In Didier Galmiche and Dominique Larchey-Wendling, editors, Tableaux 2013 -- Automated Reasoning with Analytic Tableaux and Related Methods, volume 8123 of Lecture Notes in Artificial Intelligence, pages 28--43. Springer, 2013.
Copyright Springer Verlag http://www.springer.de/comp/lncs/index.html. [pdf]