READMEs: fix publication links

PDFs and abstracts have moved to trustworthy.systems/ Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4 · Aug 25, 2021 · 81b95eb · 81b95eb
1 parent 349309e
commit 81b95eb
Show file tree

Hide file tree

Showing 19 changed files with 25 additions and 25 deletions.
diff --git a/README.md b/README.md
@@ -125,7 +125,7 @@ The repository is organised as follows.
     systems.
 
 
-  [6]: https://ts.data61.csiro.au/publications/nictaabstracts/Matichuk_WM_14.abstract "An Isabelle Proof Method Language"
+  [6]: https://trustworthy.systems/publications/nictaabstracts/Matichuk_WM_14.abstract "An Isabelle Proof Method Language"
 
 
 Hardware requirements

diff --git a/lib/EVTutorial/document/root.bib b/lib/EVTutorial/document/root.bib
@@ -13,7 +13,7 @@ @inproceedings{Murray_MBGK_12
     title            = {Noninterference for Operating System Kernels},
     pages            = {126--142},
     booktitle        = {International Conference on Certified Programs and Proofs},
-    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/6004.pdf},
+    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6004.pdf},
     publisher        = {Springer},
     isbn             = {978-3-642-35307-9}
   }

diff --git a/proof/access-control/README.md b/proof/access-control/README.md
@@ -18,7 +18,7 @@ These properties are phrased over seL4's
 [abstract specification](../../spec/abstract/) and this proof builds on
 top of the [Abstract Spec Invariant Proof](../invariant-abstract/).
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_WGMAK_11.abstract "seL4 Enforces Integrity"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Sewell_WGMAK_11.abstract "seL4 Enforces Integrity"
 
 
 Building

diff --git a/proof/asmrefine/README.md b/proof/asmrefine/README.md
@@ -23,7 +23,7 @@ PLDI '13 [paper][1].
 These theories are specific to seL4, and build on the more general apparatus
 in the [tools directory](../../tools/asmrefine).
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_MK_13.abstract  "Translation Validation for a Verified OS Kernel"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Sewell_MK_13.abstract  "Translation Validation for a Verified OS Kernel"
 
 Important Theories
 ------------------

diff --git a/proof/capDL-api/README.md b/proof/capDL-api/README.md
@@ -19,7 +19,7 @@ scheduling. These proofs are used by the [system initialiser
 proof](../../sys-init), as described in the [ICFEM '13 paper][Boyton_13]
 and Andrew Boyton's PhD thesis.
 
-  [Boyton_13]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
+  [Boyton_13]: https://trustworthy.systems/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
 
 Building
 --------

diff --git a/proof/crefine/README.md b/proof/crefine/README.md
@@ -25,7 +25,7 @@ its abstract specification.
 The approach used for the proof is described in the TPHOLS '09
 [paper][5].
 
-  [paper]: https://ts.data61.csiro.au/publications/nictaabstracts/Winwood_KSACN_09.abstract  "Mind the gap: A verification framework for low-level C"
+  [paper]: https://trustworthy.systems/publications/nictaabstracts/Winwood_KSACN_09.abstract  "Mind the gap: A verification framework for low-level C"
 
 Building
 --------

diff --git a/proof/dpolicy/Dpolicy.thy b/proof/dpolicy/Dpolicy.thy
@@ -20,7 +20,7 @@ pas_refined_transform.
 More details of this result and how it is used can be found in Section 6.1 of
 "Comprehensive Formal Verification of an OS Microkernel", which can be
 downloaded from
-https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract
+https://trustworthy.systems/publications/nictaabstracts/Klein_AEMSKH_14.abstract
 *)
 
 context begin interpretation Arch . (*FIXME: arch_split*)

diff --git a/proof/drefine/README.md b/proof/drefine/README.md
@@ -14,7 +14,7 @@ specification][capDL]. It is described as part of an ICFEM '13
 
   [aspec]: ../../spec/abstract/
   [capdl]: ../../spec/capDL/
-  [paper]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
+  [paper]: https://trustworthy.systems/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
 
 Building
 --------

diff --git a/proof/infoflow/README.md b/proof/infoflow/README.md
@@ -19,7 +19,7 @@ before transferring the noninterference result to the kernel's
 C implementation via the [Design Spec Refinement Proof](../refine/) and
 the [C Refinement Proof](../crefine/).
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Murray_MBGBSLGK_13.abstract "seL4: from General Purpose to a Proof of Information Flow Enforcement"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Murray_MBGBSLGK_13.abstract "seL4: from General Purpose to a Proof of Information Flow Enforcement"
 
 Building
 --------

diff --git a/proof/invariant-abstract/README.md b/proof/invariant-abstract/README.md
@@ -12,7 +12,7 @@ This proof defines and proves the global invariants of seL4's
 phrased and proved using a [monadic Hoare logic](../../lib/Monad_WP/NonDetMonad.thy)
 described in a TPHOLS '08 [paper][1].
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement"
 
 Building
 --------

diff --git a/proof/refine/README.md b/proof/refine/README.md
@@ -15,7 +15,7 @@ design specification, and builds on the [Abstract Spec Invariant
 Proof](../invariant-abstract/). It is described in the TPHOLS '08
 [paper][1].
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement"
 
 Building
 --------

diff --git a/proof/sep-capDL/README.md b/proof/sep-capDL/README.md
@@ -23,8 +23,8 @@ and the [system initialiser](../../sys-init/) specification.
 This separation logic is described in the [ICFEM '13 paper][Boyton_13]
 and Andrew Boyton's PhD thesis.
 
-  [Boyton_13]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
-  [Klein_KB_12]: https://ts.data61.csiro.au/publications/nictaabstracts/Klein_KB_12.abstract "Mechanised separation algebra"
+  [Boyton_13]: https://trustworthy.systems/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
+  [Klein_KB_12]: https://trustworthy.systems/publications/nictaabstracts/Klein_KB_12.abstract "Mechanised separation algebra"
 
 
 Building

diff --git a/spec/abstract/document/root.bib b/spec/abstract/document/root.bib
@@ -86,7 +86,7 @@ @TechReport{elkaduwe_ge_07
   year		= 2007,
   month		= oct,
   note		= {Available from
-		  \url{https://ts.data61.csiro.au/publications/nicta_full_text/1474.pdf}}
+		  \url{https://trustworthy.systems/publications/nicta_full_text/1474.pdf}}
 		  ,
   format	= {pdf},
   number	= {NRL-1474},

diff --git a/sys-init/README.md b/sys-init/README.md
@@ -17,7 +17,7 @@ a [separation logic defined for capDL](../proof/sep-capDL/).
 The system initialiser and the proof are described in the
 [ICFEM '13 paper][Boyton_13] and Andrew Boyton's PhD thesis.
 
-  [Boyton_13]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
+  [Boyton_13]: https://trustworthy.systems/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract "Formally Verified System Initialisation"
 
 Building
 --------

diff --git a/tools/README.md b/tools/README.md
@@ -28,5 +28,5 @@ more of the seL4 [proofs](../proof/). Each has its own directory:
  * [proofcount](proofcount/) - Tool for collecting metrics from
    finished proofs.
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Greenaway_LAK_14.abstract "Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Greenaway_LAK_14.abstract "Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain"
 
diff --git a/tools/asmrefine/README.md b/tools/asmrefine/README.md
@@ -22,7 +22,7 @@ An overview of the full proof is given with the [SydTV tool](
 https://github.com/seL4proj/graph-refine). It is also described in the
 PLDI '13 [paper][1].
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_MK_13.abstract "Translation Validation for a Verified OS Kernel"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Sewell_MK_13.abstract "Translation Validation for a Verified OS Kernel"
 
 Important Theories
 ------------------

diff --git a/tools/autocorres/README.md b/tools/autocorres/README.md
@@ -299,7 +299,7 @@ L1 (SimplConv), L2 (LocalVarExtract) and TS (TypeStrengthen) were described in
     David Greenaway, June Andronick, Gerwin Klein
     Proceedings of the Third International
             Conference on Interactive Theorem Proving (ITP), August 2012.
-    https://ts.data61.csiro.au/publications/nicta_full_text/5662.pdf
+    https://trustworthy.systems/publications/nicta_full_text/5662.pdf
 
 HL (heap abstraction) and WA (word abstraction) were described in
 
@@ -308,11 +308,11 @@ HL (heap abstraction) and WA (word abstraction) were described in
     David Greenaway, Japheth Lim, June Andronick, Gerwin Klein
     Proceedings of the 35th ACM SIGPLAN Conference on
             Programming Language Design and Implementation. ACM, June 2014.
-    https://ts.data61.csiro.au/publications/nicta_full_text/7629.pdf
+    https://trustworthy.systems/publications/nicta_full_text/7629.pdf
 
 A more comprehensive source is
 
     "Automated proof-producing abstraction of C code"
     David Greenaway
     PhD thesis, March 2015.
-    https://ts.data61.csiro.au/publications/nicta_full_text/8758.pdf
+    https://trustworthy.systems/publications/nicta_full_text/8758.pdf
diff --git a/tools/autocorres/doc/quickstart/document/root.bib b/tools/autocorres/doc/quickstart/document/root.bib
@@ -74,7 +74,7 @@ @article{Greenaway_AK_12
     booktitle        = itp12,
     pages            = {99-115},
     address          = {Princeton, New Jersey},
-    url              = {https://ts.data61.csiro.au/publications/nicta_full_text/5662.pdf}
+    url              = {https://trustworthy.systems/publications/nicta_full_text/5662.pdf}
 }
 
 @article{Greenaway_LAK_14,
@@ -89,5 +89,5 @@ @article{Greenaway_LAK_14
     type             = {Conference Paper},
     booktitle        = {Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation},
     address          = {Edinburgh, UK},
-    url              = {https://ts.data61.csiro.au/publications/nicta_full_text/7629.pdf}
+    url              = {https://trustworthy.systems/publications/nicta_full_text/7629.pdf}
 }
diff --git a/tools/autocorres/tools/release_files/README b/tools/autocorres/tools/release_files/README
@@ -329,7 +329,7 @@ L1 (SimplConv), L2 (LocalVarExtract) and TS (TypeStrengthen) were described in
     David Greenaway, June Andronick, Gerwin Klein
     Proceedings of the Third International
             Conference on Interactive Theorem Proving (ITP), August 2012.
-    https://ts.data61.csiro.au/publications/nicta_full_text/5662.pdf
+    https://trustworthy.systems/publications/nicta_full_text/5662.pdf
 
 HL (heap abstraction) and WA (word abstraction) were described in
 
@@ -338,11 +338,11 @@ HL (heap abstraction) and WA (word abstraction) were described in
     David Greenaway, Japheth Lim, June Andronick, Gerwin Klein
     Proceedings of the 35th ACM SIGPLAN Conference on
             Programming Language Design and Implementation. ACM, June 2014.
-    https://ts.data61.csiro.au/publications/nicta_full_text/7629.pdf
+    https://trustworthy.systems/publications/nicta_full_text/7629.pdf
 
 A more comprehensive source is
 
     "Automated proof-producing abstraction of C code"
     David Greenaway
     PhD thesis, March 2015.
-    https://ts.data61.csiro.au/publications/nicta_full_text/8758.pdf
+    https://trustworthy.systems/publications/nicta_full_text/8758.pdf