diff --git a/thys/Separation_Logic_Unbounded/document/root.bib b/thys/Separation_Logic_Unbounded/document/root.bib
--- a/thys/Separation_Logic_Unbounded/document/root.bib
+++ b/thys/Separation_Logic_Unbounded/document/root.bib
@@ -1,167 +1,171 @@
 @inproceedings{Dockins2009,
 author = {Dockins, Robert and Hobor, Aquinas and Appel, Andrew W.},
 pages = {161--177},
 title = {{A Fresh Look at Separation Algebras and Share Accounting}},
 booktitle = {Asian Symposium on Programming Languages and Systems (APLAS)},
 editor    = {Zhenjiang Hu},
 year = {2009}
 }
 
 @inproceedings{Calcagno2007,
 author = {Calcagno, Cristiano and O'Hearn, Peter W. and Yang, Hongseok},
 pages = {366--375},
 title = {{Local Action and Abstract Separation Logic}},
 booktitle = {Logic in Computer Science (LICS)},
 year = {2007}
 }
 
 @inproceedings{Reynolds02a,
 	author = {J. C. Reynolds},
 	title = {{Separation Logic: A Logic for Shared Mutable Data Structures}},
 	booktitle = {Logic in Computer Science (LICS)},
 	Publisher = {IEEE},
 	pages     = {55--74},
 	year = {2002}
 }
 
-
 @article{UnboundedSL,
-author = {Dardinier, Thibault and M\"uller, Peter and Summers, Alexander J.},
+author = {Dardinier, Thibault and M\"{u}ller, Peter and Summers, Alexander J.},
 title = {Fractional Resources in Unbounded Separation Logic},
 year = {2022},
 issue_date = {October 2022},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
+volume = {6},
 number = {OOPSLA2},
+url = {https://doi.org/10.1145/3563326},
+doi = {10.1145/3563326},
 journal = {Proc. ACM Program. Lang.},
-note = {To appear}
+month = {oct},
+articleno = {163},
+numpages = {27},
+keywords = {combinability, magic wands, Fractional permissions, (co)inductive predicates, automatic deductive verifiers}
 }
 
-
 @InProceedings{Wands22,
 author="Dardinier, Thibault
 and Parthasarathy, Gaurav
 and Weeks, No{\'e}
 and M{\"u}ller, Peter
 and Summers, Alexander J.",
 editor="Shoham, Sharon
 and Vizel, Yakir",
 title="Sound Automation of Magic Wands",
 booktitle="Computer Aided Verification",
 year="2022",
 publisher="Springer International Publishing",
 address="Cham",
 pages="130--151",
 isbn="978-3-031-13188-2"
 }
 
 
 @inproceedings{Boyland03,
 author="Boyland, John",
 editor="Cousot, Radhia",
 title="Checking Interference with Fractional Permissions",
 booktitle="Static Analysis (SAS)",
 year="2003",
 pages="55--72",
 }
 
 @inproceedings{BornatCOP05,
   author    = {Richard Bornat and
                Cristiano Calcagno and
                Peter W. O'Hearn and
                Matthew J. Parkinson},
   title     = {Permission accounting in separation logic},
  booktitle = {Principle of Programming Languages (POPL)},
   year      = {2005},
   pages     = {259-270},
   editor    = {Jens Palsberg and
                Mart\'{\i}n Abadi},
   publisher = {ACM}
 }
 
 @inproceedings{Brotherston20,
 author="Brotherston, James
 and Costa, Diana
 and Hobor, Aquinas
 and Wickerson, John",
 editor="Lahiri, Shuvendu K.
 and Wang, Chao",
 title="Reasoning over Permissions Regions in Concurrent Separation Logic",
 booktitle="Computer Aided Verification (CAV)",
 year="2020"
 }
 
 @inproceedings{LeHobor18,
 author="Le, Xuan-Bach
 and Hobor, Aquinas",
 editor="Ahmed, Amal",
 title="Logical Reasoning for Disjoint Permissions",
 booktitle="European Symposium on Programming (ESOP)",
 year="2018"
 }
 
 @InProceedings{LeinoMuellerSmans09,
    author    = {K. Rustan M. Leino and Peter M\"uller and Jan Smans},
   title = {Verification of Concurrent Programs with {Chalice}},
   booktitle = {Foundations of Security Analysis and Design~{V}},
   year      = {2009},
   series = {Lecture Notes in Computer Science},
   publisher = {Springer},
   url = {http://www.springerlink.com},
   urltext = {Springer-Online},
   volume = {5705},
   pages = {195-222}
 } 
 
 @InProceedings{vercors2017,
 author="Blom, Stefan
 and Darabi, Saeed
 and Huisman, Marieke
 and Oortwijn, Wytse",
 editor="Polikarpova, Nadia
 and Schneider, Steve",
 title="The {VerCors} Tool Set: Verification of Parallel and Concurrent Software",
 booktitle="Integrated Formal Methods",
 year="2017",
 publisher="Springer International Publishing",
 address="Cham",
 pages="102--110",
 isbn="978-3-319-66845-1"
 }
 
 
 
 
 @inproceedings{MuellerSchwerhoffSummers16,
  author = {Peter M{\"u}ller and Malte Schwerhoff and Alexander J. Summers},
  title = {Viper: A Verification Infrastructure for Permission-Based Reasoning},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  editor = {B. Jobstmann and K. R. M. Leino},
  year = {2016},
  publisher = {Springer},
  series = LNCS,
  pages = {41-62},
  volume = {9583}
 }
 
 @inproceedings{JacobsSPVPP11,
   author    = {Bart Jacobs and
                Jan Smans and
                Pieter Philippaerts and
                Fr{\'e}d{\'e}ric Vogels and
                Willem Penninckx and
                Frank Piessens},
   title     = {{VeriFast}: A Powerful, Sound, Predictable, Fast Verifier
                for {C} and {J}ava},
   booktitle = {NASA Formal Methods (NFM)},
   year      = {2011},
   pages     = {41-55},
   editor    = {Mihaela Gheorghiu Bobaru and
                Klaus Havelund and
                Gerard J. Holzmann and
                Rajeev Joshi},
   publisher = {Springer},
   series    = {Lecture Notes in Computer Science},
   volume    = {6617}
 }