A Hoare Logic for Diverging Programs by Johannes Åman Pohjola, Magnus O. Myreen and Miki Tanaka Jan 20