book: Add links to KISV 2023 paper and GOSIM 2023 presentation (#1062) …

…a859ff5
theseus-os · Oct 23, 2023 · 167584e · 167584e
1 parent 7e6fe38
commit 167584e
Show file tree

Hide file tree

Showing 4 changed files with 42 additions and 16 deletions.
diff --git a/book/misc/papers_presentations.html b/book/misc/papers_presentations.html
@@ -148,7 +148,8 @@ <h1 id="papers-and-presentations-about-theseus"><a class="header" href="#papers-
 This page offers a selected collection of the slide decks from those talks (including some video recordings), as well as a list of selected peer-reviewed academic publications and theses.</p>
 <h2 id="selected-papers-and-theses"><a class="header" href="#selected-papers-and-theses">Selected Papers and Theses</a></h2>
 <ul>
-<li>[OSDI 2020] <strong><a href="https://www.usenix.org/conference/osdi20/presentation/boos">Theseus: an Experiment in Operating System Structure and State Management</a></strong>
+<li>
+<p>[OSDI 2020] <strong><a href="https://www.usenix.org/conference/osdi20/presentation/boos">Theseus: an Experiment in Operating System Structure and State Management</a></strong></p>
 <ul>
 <li>The main paper describing Theseus's design principles, implementation, evaluation, and limitations.</li>
 <li><a href="https://www.usenix.org/system/files/osdi20-boos.pdf">Paper (PDF)</a> — 
@@ -157,17 +158,28 @@ <h2 id="selected-papers-and-theses"><a class="header" href="#selected-papers-and
 <a href="https://www.usenix.org/sites/default/files/conference/protected-files/osdi20_slides_boos.pdf">Slides (PDF)</a></li>
 </ul>
 </li>
+<li>
+<p>[<a href="https://kisv-workshop.github.io/program/">KISV 2023</a>] <strong><a href="https://dl.acm.org/doi/10.1145/3625275.3625398">Leveraging Rust for Lightweight OS Correctness</a></strong></p>
+<ul>
+<li>A paper about extending intralingual design and applying a hybrid approach (type systems plus formal verification) for proving lightweight correctness guarantees about Theseus's memory management subsystem.</li>
+<li><a href="https://dl.acm.org/doi/pdf/10.1145/3625275.3625398">Paper (PDF)</a></li>
+</ul>
+</li>
+<li>
+<p>Kevin Boos PhD Dissertation: <a href="https://scholarship.rice.edu/handle/1911/109201">Theseus: Rethinking Operating Systems Structure and State Management</a></p>
+</li>
+<li>
+<p>Ramla Ijaz Master's Thesis: <a href="https://scholarship.rice.edu/handle/1911/109609">Exploring Intralingual Design in Operating Systems</a></p>
+</li>
+</ul>
+<h3 id="other-published-works"><a class="header" href="#other-published-works">Other published works</a></h3>
+<ul>
 <li>[OSDI 2022] Poster: <a href="https://www.usenix.org/conference/osdi22/poster-session">Correct and Performant Device Drivers via Intralingual Design</a>
 <ul>
 <li>An overview of in-progress work to use formal verification + intralingual design for better device drivers.</li>
 <li><a href="https://www.theseus-os.com/kevinaboos/docs/OSDI%202022%20Poster.pdf">Poster PDF</a></li>
 </ul>
 </li>
-<li>Kevin Boos PhD Dissertation: <a href="https://scholarship.rice.edu/handle/1911/109201">Theseus: Rethinking Operating Systems Structure and State Management</a></li>
-<li>Ramla Ijaz Master's Thesis: <a href="https://scholarship.rice.edu/handle/1911/109609">Exploring Intralingual Design in Operating Systems</a></li>
-</ul>
-<h3 id="older-papers"><a class="header" href="#older-papers">Older papers</a></h3>
-<ul>
 <li>[PLOS 2017] <a href="https://www.sigops.org/s/conferences/sosp/2017/workshops.html">Theseus: A State Spill-free Operating System</a>
 <ul>
 <li><a href="https://www.theseus-os.com/kevinaboos/docs/theseus_plos2017.pdf">Paper PDF</a> — a shorter, outdated ideas paper about early Theseus design.</li>
@@ -183,6 +195,7 @@ <h3 id="older-papers"><a class="header" href="#older-papers">Older papers</a></h
 </ul>
 <h2 id="selected-presentations-and-slide-decks"><a class="header" href="#selected-presentations-and-slide-decks">Selected Presentations and Slide Decks</a></h2>
 <ul>
+<li><a href="https://docs.google.com/presentation/d/e/2PACX-1vSq144Pl5Ql02OP9zq80wuy7iI1GwUNfCwUelpKay2qeIis4uMY2qOfSgIKeG7Rb053fMoVXXHa3ka9/pub?start=false&amp;loop=false">Theseus: a Rust-native OS for Safety and Reliability (Sept 2023)</a> – [<a href="https://www.bilibili.com/video/BV1d34y1373n/">Video talk</a>]</li>
 <li><a href="https://docs.google.com/presentation/d/e/2PACX-1vQ2InjW_5kpdepoJ9vdsH-B1G4mvcjohcj_CA2dzx-tVRz0ee52qo1bwCQ7TnDGE9PiE5doW4sIO_7W/pub?start=false&amp;loop=false">How Theseus uses Rust, plus Rust challenges (early 2022)</a></li>
 <li><a href="https://docs.google.com/presentation/d/e/2PACX-1vSa0gp8sbq8S9MB4V-FYjs6xJGIPm0fsZSVdtZ9U2bQWRX9gngwztXTIJiRwxtAosLWPk0v60abDMTU/pub?start=false&amp;loop=false">How Safe-language OSes work, with Theseus examples</a> — 
 [<a href="https://www.youtube.com/watch?v=n7r8zO7SodE">Video Talk</a>]</li>
@@ -203,7 +216,7 @@ <h2 id="selected-presentations-and-slide-decks"><a class="header" href="#selecte
 <li><a href="https://docs.google.com/presentation/d/e/2PACX-1vQYomAnfTNucuCqYgNkPaxpIdrhPxil9Qzle_6-xd7TYfdEBlgML0B3vztdNC2odwc25dLzW3XsithZ/pub?start=false&amp;loop=false">Rust vs. C, with short Rust intro</a> — 
 [<a href="https://www.youtube.com/watch?v=mmJiwscpB4o">Video Talk</a>]</li>
 </ul>
-<!-- cspell:ignore OSDI, PLOS, Ramla Ijaz -->
+<!-- cspell:ignore OSDI, PLOS, KISV, Ramla Ijaz -->
 
                     </main>
 

diff --git a/book/print.html b/book/print.html
@@ -1785,7 +1785,8 @@ <h3 id="double-check-commit-contents"><a class="header" href="#double-check-comm
 This page offers a selected collection of the slide decks from those talks (including some video recordings), as well as a list of selected peer-reviewed academic publications and theses.</p>
 <h2 id="selected-papers-and-theses"><a class="header" href="#selected-papers-and-theses">Selected Papers and Theses</a></h2>
 <ul>
-<li>[OSDI 2020] <strong><a href="https://www.usenix.org/conference/osdi20/presentation/boos">Theseus: an Experiment in Operating System Structure and State Management</a></strong>
+<li>
+<p>[OSDI 2020] <strong><a href="https://www.usenix.org/conference/osdi20/presentation/boos">Theseus: an Experiment in Operating System Structure and State Management</a></strong></p>
 <ul>
 <li>The main paper describing Theseus's design principles, implementation, evaluation, and limitations.</li>
 <li><a href="https://www.usenix.org/system/files/osdi20-boos.pdf">Paper (PDF)</a> — 
@@ -1794,17 +1795,28 @@ <h2 id="selected-papers-and-theses"><a class="header" href="#selected-papers-and
 <a href="https://www.usenix.org/sites/default/files/conference/protected-files/osdi20_slides_boos.pdf">Slides (PDF)</a></li>
 </ul>
 </li>
+<li>
+<p>[<a href="https://kisv-workshop.github.io/program/">KISV 2023</a>] <strong><a href="https://dl.acm.org/doi/10.1145/3625275.3625398">Leveraging Rust for Lightweight OS Correctness</a></strong></p>
+<ul>
+<li>A paper about extending intralingual design and applying a hybrid approach (type systems plus formal verification) for proving lightweight correctness guarantees about Theseus's memory management subsystem.</li>
+<li><a href="https://dl.acm.org/doi/pdf/10.1145/3625275.3625398">Paper (PDF)</a></li>
+</ul>
+</li>
+<li>
+<p>Kevin Boos PhD Dissertation: <a href="https://scholarship.rice.edu/handle/1911/109201">Theseus: Rethinking Operating Systems Structure and State Management</a></p>
+</li>
+<li>
+<p>Ramla Ijaz Master's Thesis: <a href="https://scholarship.rice.edu/handle/1911/109609">Exploring Intralingual Design in Operating Systems</a></p>
+</li>
+</ul>
+<h3 id="other-published-works"><a class="header" href="#other-published-works">Other published works</a></h3>
+<ul>
 <li>[OSDI 2022] Poster: <a href="https://www.usenix.org/conference/osdi22/poster-session">Correct and Performant Device Drivers via Intralingual Design</a>
 <ul>
 <li>An overview of in-progress work to use formal verification + intralingual design for better device drivers.</li>
 <li><a href="https://www.theseus-os.com/kevinaboos/docs/OSDI%202022%20Poster.pdf">Poster PDF</a></li>
 </ul>
 </li>
-<li>Kevin Boos PhD Dissertation: <a href="https://scholarship.rice.edu/handle/1911/109201">Theseus: Rethinking Operating Systems Structure and State Management</a></li>
-<li>Ramla Ijaz Master's Thesis: <a href="https://scholarship.rice.edu/handle/1911/109609">Exploring Intralingual Design in Operating Systems</a></li>
-</ul>
-<h3 id="older-papers"><a class="header" href="#older-papers">Older papers</a></h3>
-<ul>
 <li>[PLOS 2017] <a href="https://www.sigops.org/s/conferences/sosp/2017/workshops.html">Theseus: A State Spill-free Operating System</a>
 <ul>
 <li><a href="https://www.theseus-os.com/kevinaboos/docs/theseus_plos2017.pdf">Paper PDF</a> — a shorter, outdated ideas paper about early Theseus design.</li>
@@ -1820,6 +1832,7 @@ <h3 id="older-papers"><a class="header" href="#older-papers">Older papers</a></h
 </ul>
 <h2 id="selected-presentations-and-slide-decks"><a class="header" href="#selected-presentations-and-slide-decks">Selected Presentations and Slide Decks</a></h2>
 <ul>
+<li><a href="https://docs.google.com/presentation/d/e/2PACX-1vSq144Pl5Ql02OP9zq80wuy7iI1GwUNfCwUelpKay2qeIis4uMY2qOfSgIKeG7Rb053fMoVXXHa3ka9/pub?start=false&amp;loop=false">Theseus: a Rust-native OS for Safety and Reliability (Sept 2023)</a> – [<a href="https://www.bilibili.com/video/BV1d34y1373n/">Video talk</a>]</li>
 <li><a href="https://docs.google.com/presentation/d/e/2PACX-1vQ2InjW_5kpdepoJ9vdsH-B1G4mvcjohcj_CA2dzx-tVRz0ee52qo1bwCQ7TnDGE9PiE5doW4sIO_7W/pub?start=false&amp;loop=false">How Theseus uses Rust, plus Rust challenges (early 2022)</a></li>
 <li><a href="https://docs.google.com/presentation/d/e/2PACX-1vSa0gp8sbq8S9MB4V-FYjs6xJGIPm0fsZSVdtZ9U2bQWRX9gngwztXTIJiRwxtAosLWPk0v60abDMTU/pub?start=false&amp;loop=false">How Safe-language OSes work, with Theseus examples</a> — 
 [<a href="https://www.youtube.com/watch?v=n7r8zO7SodE">Video Talk</a>]</li>
@@ -1840,7 +1853,7 @@ <h2 id="selected-presentations-and-slide-decks"><a class="header" href="#selecte
 <li><a href="https://docs.google.com/presentation/d/e/2PACX-1vQYomAnfTNucuCqYgNkPaxpIdrhPxil9Qzle_6-xd7TYfdEBlgML0B3vztdNC2odwc25dLzW3XsithZ/pub?start=false&amp;loop=false">Rust vs. C, with short Rust intro</a> — 
 [<a href="https://www.youtube.com/watch?v=mmJiwscpB4o">Video Talk</a>]</li>
 </ul>
-<!-- cspell:ignore OSDI, PLOS, Ramla Ijaz -->
+<!-- cspell:ignore OSDI, PLOS, KISV, Ramla Ijaz -->
 <div style="break-before: page; page-break-before: always;"></div><h1 id="theseus-readme--quick-start"><a class="header" href="#theseus-readme--quick-start">Theseus README + Quick Start</a></h1>
 <p><a href="https://github.com/theseus-os/Theseus/blob/theseus_main/README.md">Click here to see the main Theseus README for quick start instructions.</a></p>
 

diff --git a/book/searchindex.js b/book/searchindex.js
diff --git a/book/searchindex.json b/book/searchindex.json