@misc{indiciaeb745bfd0b40e, title = {Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)}, author = {Pedro Barroso and Mário Pereira and António Ravara}, year = {2022}, url = {https://arxiv.org/abs/2212.02425}, note = {Source identifier: 2212.02425} }