From ba38ae33ab1e6f920d0ff0fcaa774a3ce0a29ff4 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 23 Nov 2020 16:56:45 +1100 Subject: [PATCH] update publications links The links to nicta.com.au have stopped working, so the publication links now point to the TS publication pages. Signed-off-by: Gerwin Klein --- README.md | 2 +- proof/access-control/README.md | 2 +- proof/asmrefine/README.md | 2 +- proof/capDL-api/README.md | 2 +- proof/crefine/README.md | 2 +- proof/drefine/README.md | 2 +- proof/infoflow/README.md | 2 +- proof/invariant-abstract/README.md | 2 +- proof/refine/README.md | 2 +- proof/sep-capDL/README.md | 4 ++-- sys-init/README.md | 2 +- tools/README.md | 2 +- tools/asmrefine/README.md | 2 +- 13 files changed, 14 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index be80b4149..efb97eb06 100644 --- a/README.md +++ b/README.md @@ -172,7 +172,7 @@ The repository is organised as follows. systems. - [6]: http://www.nicta.com.au/pub?id=7847 "An Isabelle Proof Method Language" + [6]: https://ts.data61.csiro.au/publications/nictaabstracts/Matichuk_WM_14.abstract.pml "An Isabelle Proof Method Language" Hardware requirements diff --git a/proof/access-control/README.md b/proof/access-control/README.md index 6a43d2fee..7b0325fa3 100644 --- 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]: http://www.nicta.com.au/pub?id=4709 "seL4 Enforces Integrity" + [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_WGMAK_11.abstract.pml "seL4 Enforces Integrity" Building diff --git a/proof/asmrefine/README.md b/proof/asmrefine/README.md index 4b06833c0..d939d0c4b 100644 --- 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]: http://www.nicta.com.au/pub?id=6449 "Translation Validation for a Verified OS Kernel" + [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_MK_13.abstract.pml "Translation Validation for a Verified OS Kernel" Important Theories ------------------ diff --git a/proof/capDL-api/README.md b/proof/capDL-api/README.md index 42b425361..dac0b2f6a 100644 --- 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]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation" + [Boyton_13]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract.pml "Formally Verified System Initialisation" Building -------- diff --git a/proof/crefine/README.md b/proof/crefine/README.md index 9969540ba..0b686ff48 100644 --- 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]: http://www.nicta.com.au/pub?id=1842 " Mind the gap: A verification framework for low-level C" + [paper]: https://ts.data61.csiro.au/publications/nictaabstracts/Winwood_KSACN_09.abstract.pml "Mind the gap: A verification framework for low-level C" Building -------- diff --git a/proof/drefine/README.md b/proof/drefine/README.md index a73d9b77d..50f766a25 100644 --- 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]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation" + [paper]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract.pml "Formally Verified System Initialisation" Building -------- diff --git a/proof/infoflow/README.md b/proof/infoflow/README.md index 657535e4b..b9a71ff31 100644 --- 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]: http://www.nicta.com.au/pub?id=6464 "seL4: from General Purpose to a Proof of Information Flow Enforcement" + [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Murray_MBGBSLGK_13.abstract.pml "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 index 3daefeb18..c99faffe9 100644 --- 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]: http://nicta.com.au/pub?id=483 "Secure Microkernels, State Monads and Scalable Refinement" + [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Cock_KS_08.abstract.pml "Secure Microkernels, State Monads and Scalable Refinement" Building -------- diff --git a/proof/refine/README.md b/proof/refine/README.md index ef86a9c06..783395ba3 100644 --- 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]: http://nicta.com.au/pub?id=483 "Secure Microkernels, State Monads and Scalable Refinement" + [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Cock_KS_08.abstract.pml "Secure Microkernels, State Monads and Scalable Refinement" Building -------- diff --git a/proof/sep-capDL/README.md b/proof/sep-capDL/README.md index 147b44a8e..21683a333 100644 --- 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]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation" - [Klein_KB_12]: http://www.nicta.com.au/pub?id=5676 "Mechanised separation algebra" + [Boyton_13]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract.pml "Formally Verified System Initialisation" + [Klein_KB_12]: https://ts.data61.csiro.au/publications/nictaabstracts/Klein_KB_12.abstract.pml "Mechanised separation algebra" Building diff --git a/sys-init/README.md b/sys-init/README.md index 46ff51366..75230bbb6 100644 --- 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]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation" + [Boyton_13]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract.pml "Formally Verified System Initialisation" Building -------- diff --git a/tools/README.md b/tools/README.md index 562d20cb7..0fa03fc1b 100644 --- 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]: http://www.nicta.com.au/pub?id=7629 "Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain" + [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Greenaway_LAK_14.abstract.pml "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 index fd9730e7a..d5388530f 100644 --- 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]: http://www.nicta.com.au/pub?id=6449 "Translation Validation for a Verified OS Kernel" + [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_MK_13.abstract.pml "Translation Validation for a Verified OS Kernel" Important Theories ------------------