adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

READMEs: fix publication links 

PDFs and abstracts have moved to trustworthy.systems/

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-08-25 10:50:38 +10:00 committed by Gerwin Klein
parent 349309ebf5
commit 81b95eb6bf
19 changed files with 25 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.md
View File

@ -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

2
lib/EVTutorial/document/root.bib
View File

@ -13,7 +13,7 @@
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}
}

2
proof/access-control/README.md
View File

@ -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

2
proof/asmrefine/README.md
View File

@ -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
------------------

2
proof/capDL-api/README.md
View File

@ -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
--------

2
proof/crefine/README.md
View File

@ -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
--------

2
proof/dpolicy/Dpolicy.thy
View File

@ -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*)

2
proof/drefine/README.md
View File

@ -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
--------

2
proof/infoflow/README.md
View File

@ -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
--------

2
proof/invariant-abstract/README.md
View File

@ -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
--------

2
proof/refine/README.md
View File

@ -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
--------

4
proof/sep-capDL/README.md
View File

@ -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

2
spec/abstract/document/root.bib
View File

@ -86,7 +86,7 @@
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},

2
sys-init/README.md
View File

@ -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
--------

2
tools/README.md
View File

@ -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"

2
tools/asmrefine/README.md
View File

@ -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
------------------

6
tools/autocorres/README.md
View File

@ -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

4
tools/autocorres/doc/quickstart/document/root.bib
View File

@ -74,7 +74,7 @@
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 @@
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}
}

6
tools/autocorres/tools/release_files/README
View File

@ -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