Fix paper URLs

Signed-off-by: Gernot Heiser <[email protected]>
seL4 · May 7, 2024 · 9fefcc9 · 9fefcc9
1 parent 0b6d1c3
commit 9fefcc9
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 32 deletions.
diff --git a/Makefile b/Makefile
@@ -270,7 +270,6 @@ $(Bib): $(addsuffix .tex, $(Targets))
 		${sed} <tmp.bib > $(Bib) \
 			-e 's/^ *isbn *= *{/  NOisbn = {/' \
 			-e 's/^ *issn *= *{/  NOissn = {/' \
-			-e 's/^ *doi *= *{/  NOdoi = {/' \
 			-e 's/^ *editor *= *{/  NOeditor = {/' \
 			-e 's/^ *paper[uU]rl *=/  url =/'; \
 		cp tmp.aux references.aux; \

diff --git a/references.bib b/references.bib
@@ -28,12 +28,11 @@ @inproceedings{Biggs_LH_18
   month =         aug,
   numpages =      {7},
   publisher =     {ACM SIGOPS},
-  type =          {Conference Paper - Refereed},
   title =         {The Jury Is In: Monolithic {OS} Design Is Flawed},
   year =          {2018},
-  NOdoi = {https://doi.org/10.1145/3265723.3265733},
+  doi =           {https://doi.org/10.1145/3265723.3265733},
   url =
-  {https://ts.data61.csiro.au/publications/csiro_full_text//Biggs_LH_18.pdf},
+  {https://trustworthy.systems/publications/full_text/Biggs_LH_18.pdf},
 }
 
 @inproceedings{Blackham_SCRH_11,
@@ -49,7 +48,7 @@ @inproceedings{Blackham_SCRH_11
                    Kernel},
   year =          {2011},
   url =
-  {https://ts.data61.csiro.au/publications/nicta_full_text/4863.pdf},
+  {https://trustworthy.systems/publications/nicta_full_text/4863.pdf},
 }
 
 @inproceedings{Sewell_KH_16,
@@ -62,7 +61,7 @@ @inproceedings{Sewell_KH_16
                    and Infeasible Paths for {WCET} Analysis},
   year =          {2016},
   url =
-  {https://ts.data61.csiro.au/publications/nicta_full_text/9118.pdf},
+  {https://trustworthy.systems/publications/nicta_full_text/9118.pdf},
 }
 
 @article{Sewell_KH_17,
@@ -71,14 +70,13 @@ @article{Sewell_KH_17
   month =         sep,
   pages =         {812-853},
   publisher =     {Springer},
-  type =          {Journal Article - Refereed},
   title =         {High-Assurance Timing Analysis for a High-Assurance
                    Real-Time {OS}},
   volume =        {53},
   year =          {2017},
-  NOdoi = {https://doi.org/10.1007/s11241-017-9286-3},
+  doi =           {https://doi.org/10.1007/s11241-017-9286-3},
   url =
-  {https://ts.data61.csiro.au/publications/csiro_full_text//Sewell_KH_17.pdf},
+  {https://trustworthy.systems/publications/full_text/Sewell_KH_17.pdf},
 }
 
 @inproceedings{Boebert_84,
@@ -115,11 +113,11 @@ @inproceedings{Ge_YCH_19
   month =         mar,
   numpages =      {17},
   publisher =     {ACM},
-  type =          {Conference Paper - Refereed},
   title =         {Time Protection: the Missing {OS} Abstraction},
   year =          {2019},
+  doi =           {10.1145/3302424.3303976},
   url =
-  {https://ts.data61.csiro.au/publications/csiro_full_text//Ge_YCH_19.pdf},
+  {https://trustworthy.systems/publications/full_text/Ge_YCH_19.pdf},
 }
 
 @inproceedings{Gu_SCWKSC_16,
@@ -158,9 +156,9 @@ @article{Heiser_Elphinstone_16
                    Research and Deployment},
   volume =        {34},
   year =          {2016},
-  NOdoi = {10.1145/2893177},
+  doi =           {10.1145/2893177},
   url =
-  {https://ts.data61.csiro.au/publications/nicta_full_text/8988.pdf},
+  {https://trustworthy.systems/publications/nicta_full_text/8988.pdf},
 }
 
 @inproceedings{Heiser_KM_19,
@@ -170,12 +168,11 @@ @inproceedings{Heiser_KM_19
   month =         may,
   pages =         {23-29},
   publisher =     {ACM},
-  type =          {Conference Paper - Refereed},
   title =         {Can We Prove Time Protection?},
   year =          {2019},
-  NOdoi = {https://doi.org/10.1145/3317550.3321431},
+  doi =           {https://doi.org/10.1145/3317550.3321431},
   url =
-  {https://ts.data61.csiro.au/publications/csiro_full_text//Heiser_KM_19.pdf},
+  {https://trustworthy.systems/publications/full_text/Heiser_KM_19.pdf},
 }
 
 @article{Klein_AEMSKH_14,
@@ -191,22 +188,27 @@ @article{Klein_AEMSKH_14
                    Microkernel},
   volume =        {32},
   year =          {2014},
-  NOdoi = {10.1145/2560537},
+  doi =           {10.1145/2560537},
   url =
-  {https://ts.data61.csiro.au/publications/nicta_full_text/7371.pdf},
+  {https://trustworthy.systems/publications/nicta_full_text/7371.pdf},
 }
 
-@inproceedings{Klein_EHA_etal_09,
-  address =       {Big Sky, MT, US},
-  author =        {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and
-                   June Andronick and others},
+@inproceedings{Klein_EHACDEEKNSTW_09,
+  address =       {Big Sky, MT, USA},
+  author =        {Klein, Gerwin and Elphinstone, Kevin and
+                   Heiser, Gernot and Andronick, June and Cock, David and
+                   Derrin, Philip and Elkaduwe, Dhammika and
+                   Engelhardt, Kai and Kolanski, Rafal and
+                   Norrish, Michael and Sewell, Thomas and Tuch, Harvey and
+                   Winwood, Simon},
   booktitle =     {ACM Symposium on Operating Systems Principles},
   month =         oct,
   pages =         {207--220},
+  publisher =     {ACM},
   title =         {{seL4}: Formal Verification of an {OS} Kernel},
   year =          {2009},
   url =
-  {https://ts.data61.csiro.au/publications/nicta_full_text/1852.pdf},
+  {https://trustworthy.systems/publications/nicta_full_text/1852.pdf},
 }
 
 @inproceedings{Lyons_MAH_18,
@@ -217,20 +219,21 @@ @inproceedings{Lyons_MAH_18
   month =         apr,
   numpages =      {14},
   publisher =     {ACM},
-  type =          {Conference Paper - Refereed},
   title =         {Scheduling-Context Capabilities: {A} Principled,
                    Light-Weight {OS} Mechanism for Managing Time},
   year =          {2018},
   url =
-  {https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf},
+  {https://trustworthy.systems/publications/full_text/Lyons_MAH_18.pdf},
 }
 
 @inproceedings{Mi_LYWC_19,
+  address =       {Dresden, DE},
   author =        {Zeyu Mi and Dingji Li and Zihan Yang and Xinran Wang and
                    Haibo Chen},
   booktitle =     {EuroSys Conference},
   month =         mar,
   numpages =      {15},
+  publisher =     {ACM},
   title =         {{SkyBridge}: Fast and Secure Inter-Process
                    Communication for Microkernels},
   year =          {2019},

diff --git a/whitepaper.tex b/whitepaper.tex
@@ -88,11 +88,7 @@
 
   \newcommand{\gernot}[1]{\Comment{#1 \colorbox{yellow}{[gernot]}}}
 
-  \hypersetup{pdftex,
-                      pagebackref,
-                      hyperindex,
-                      bookmarks,
-                      pdftitle={The seL4 Microkernel -- An Introduction},
+  \hypersetup{pdftitle={The seL4 Microkernel -- An Introduction},
                       pdfauthor={Gernot Heiser},
                       pdfsubject={seL4 Foundation Whitepaper Revision 1.2},
                       pdfkeywords={seL4, microkernel, performance},
@@ -119,7 +115,8 @@
   \author{Gernot Heiser}
 %  \authortitle{Author's title}
   \email{[email protected]}
-  \docversion{Revision 1.2 of 2020-06-10}
+%  \docversion{Revision 1.2 of 2020-06-10} % fa89642
+  \docversion{Revision 1.3 of 2024-05-07}
   \date{}
 
   \thispagestyle{plain}
@@ -207,7 +204,7 @@
     in a very strong sense ``bug free'' with respect to its specification.
     In fact, seL4 is the world's
     first OS kernel with such a proof at the code level
-    \citep{Klein_EHA_etal_09}.
+    \citep{Klein_EHACDEEKNSTW_09}.
 
   \item[seL4 is provably secure]\Break
     Besides implementation correctness, seL4 comes with further proofs of