Alain Finkel, Étienne Lozes, Arnaud Sangnier: Towards Model-Checking Programs with Lists. ILC 2007: 56-86