diff --git a/MaksimovicExact2022.pdf b/Maksimovic2022Exact.pdf
similarity index 64%
rename from MaksimovicExact2022.pdf
rename to Maksimovic2022Exact.pdf
index 51e34b8f9a489650ba566ed0a285e18809fc3f9a..7e98faf01ad43727fdb25a82bef77f7e31d577c3 100644
Binary files a/MaksimovicExact2022.pdf and b/Maksimovic2022Exact.pdf differ
diff --git a/publications.bib b/publications.bib
index 8df0a2da22a1e424956a5e4efef2b5ec3d7988cc..645dc422a7a940ed41e56d9f52429e782420ddde 100644
--- a/publications.bib
+++ b/publications.bib
@@ -1648,7 +1648,7 @@ in JavaScript verification; and the feasibility of automatic compositional testi
 @InProceedings{Bodin2019Skeletal,
   author    = {Martin Bodin and Philippa Gardner and Thomas Jensen and Alan Schmitt},
   title     = {Skeletal Semantics and their Interpretations},
-  booktitle = {Proceedings of the 46\textsuperscript{th} {ACM} {SIGPLAN-SIGACT} 
+  booktitle = {Proceedings of the 46\textsuperscript{th} {ACM} {SIGPLAN-SIGACT}
   Symposium on Principles of Programming Languages (POPL'19)},
   volume    = {3},
   number    = {{POPL}},
@@ -1862,12 +1862,12 @@ title     = {TaDA Live: Compositional Reasoning for Termination of Fine-grained
             Concurrent Programs},
 journal   = {ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021.},
 year      = {2021},
-publisher = {Association for Computing Machinery}, 
-volume    = {43}, 
-number    = {4}, 
-issn      = {0164-0925}, 
-url       = {https://doi.org/10.1145/3477082}, 
-doi       = {10.1145/3477082}, 
+publisher = {Association for Computing Machinery},
+volume    = {43},
+number    = {4},
+issn      = {0164-0925},
+url       = {https://doi.org/10.1145/3477082},
+doi       = {10.1145/3477082},
 abstract  = {We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of
 blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking:
 that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in,
@@ -1910,9 +1910,9 @@ two bugs in the JavaScript and three bugs in the C implementation.},
 
 @InProceedings{Watt2021Two,
 author = {Conrad Watt and
-          Xiaojia Rao and 
+          Xiaojia Rao and
           Jean Pichon-Pharabod and
-          Martin Bodin and 
+          Martin Bodin and
           Philippa Gardner},
 title  = {Two Mechanisations of WebAssembly 1.0},
 booktitle = {Proceedings of the 24\textsuperscript{th} international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021},
@@ -1928,28 +1928,28 @@ url    = {https://doi.org/10.1007/978-3-030-90870-6\_4},
 doi    = {10.1007/978-3-030-90870-6\_4},
 abstract  = {WebAssembly (Wasm) is a new bytecode language supported
 by all major Web browsers, designed primarily to be an efficient compilation
-target for low-level languages such as C/C++ and Rust. It is unusual in that 
-it is officially specified through a formal semantics. An initial draft 
-specification was published in 2017 with an associated mechanised 
+target for low-level languages such as C/C++ and Rust. It is unusual in that
+it is officially specified through a formal semantics. An initial draft
+specification was published in 2017 with an associated mechanised
 specification in Isabelle/HOL published by Watt that found
-bugs in the original specification, fixed before its publication. 
+bugs in the original specification, fixed before its publication.
 The  first official W3C standard, WebAssembly 1.0, was published in
-2019. Building on Watt's original mechanisation, we introduce two 
+2019. Building on Watt's original mechanisation, we introduce two
 mechanised specifications of the WebAssembly 1.0 semantics, written
-in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. 
+in different theorem provers: WasmCert-Isabelle and WasmCert-Coq.
 Wasm's compact design and official formal semantics enable our mechanisations
-to be particularly complete and close to the published language standard. 
+to be particularly complete and close to the published language standard.
 We present a high-level description of the language's updated
-type soundness result, referencing both mechanisations. 
+type soundness result, referencing both mechanisations.
 We also describe the current state of the mechanisation of language features not previously
-supported: WasmCert-Isabelle includes a verified executable definition 
+supported: WasmCert-Isabelle includes a verified executable definition
 of the instantiation phase as part of an executable verified interpreter;
-WasmCert-Coq includes executable parsing and numeric definitions as 
+WasmCert-Coq includes executable parsing and numeric definitions as
 on-going work towards a more ambitious end-to-end verified interpreter
 which does not require an OCaml harness like WasmCert-Isabelle.},
 }
 
-@InProceedings{MaksimovicExact2022,
+@InProceedings{Maksimovic2022Exact,
 author = {Petar Maksimoví\'c and
           Caroline Cronj\"ager and
           Julian Sutherland and