A simple, verified validator for software pipelining.

Jean-Baptiste Tristan, Xavier Leroy

Browse the full POPL paper archive.