Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. - Charguéraud, Arthur; Pottier, François (Journal of Automated Reasoning, 2019)