Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron. From Relational Verification to SIMD Loop Synthesis. ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013, pages 123–134, ACM, 2013.