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

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 <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-11-23 16:56:45 +11:00 committed by Gerwin Klein
parent 898e5afc63
commit ba38ae33ab
13 changed files with 14 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.md
View File

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

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]: 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

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]: 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
------------------

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]: 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
--------

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]: 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
--------

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]: 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
--------

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]: 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
--------

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]: 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
--------

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]: 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
--------

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]: 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

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]: 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
--------

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]: 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"

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]: 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
------------------