A relational framework for bounded program verification. - Gregory D. Dennis (2009)