diff --git a/pages/2024-sosp/css/index.css b/pages/2024-sosp/css/index.css index 835d824..c1c0741 100644 --- a/pages/2024-sosp/css/index.css +++ b/pages/2024-sosp/css/index.css @@ -68,6 +68,9 @@ span.highlight-2 { color: transparent; display: inline; } +p.highlight-0 { + font-weight: bold; +} p:first-child { margin-top: 0px; @@ -123,12 +126,17 @@ span.comment { font-size: 80%; } +li { + margin-left: 20px; +} + ul.organizers { list-style-type: none; } ul.organizers > li { margin-bottom: 10px; + margin-left: 0; } ul.organizers > li:first-child { margin-top: 10px; @@ -136,3 +144,4 @@ ul.organizers > li:first-child { ul.organizers summary { cursor: pointer; } + diff --git a/pages/2024-sosp/index.html b/pages/2024-sosp/index.html index 004d476..45aa012 100644 --- a/pages/2024-sosp/index.html +++ b/pages/2024-sosp/index.html @@ -37,8 +37,8 @@

Tutorial: Verifying Rust code with + These techniques can help Systems Researchers build reliable, secure systems, with less + reliance on runtime checking, which can be expensive.

This tutorial introduces Verus, an open-source, Rust-based verification tool designed specifically for systems software. @@ -70,12 +70,13 @@

Tutorial: Verifying Rust code with - The morning program is designed to be self-contained. In the afternoon, +

The morning program is designed to be self-contained. In the afternoon, attendees can choose to switch to a different workshop, or continue working on the material and - exercises presented in the morning with the help of the organizers. + exercises presented in the morning with the help of the organizers.

- Morning Program (subject to change): +

Morning Program (tentative):

  • Overview of uses of verification, and introduction to systems verification;
  • Verus set up: how to run it and where to find documentation;
  • @@ -84,6 +85,7 @@

    Tutorial: Verifying Rust code with Primers on "quantifiers" (∀/∃), how they are used in specifications and proofs (with interactive exercise);
  • Primer on SMT solvers (underlying Verus' automation);
  • "Capstone" interactive exercise to complete with the help of the organizers.
  • +

@@ -94,16 +96,18 @@

Tutorial: Verifying Rust code with Afternoon Program (tentative):

  • How to debug a failing proof;
  • Verifying code with unsafe pointers (with interactive exercise);
  • Primer on Verus' mode system (for specification, proof, and executable code);
  • Verifying shared-memory concurrent code with VerusSync (with interactive exercise);
  • Open Q&A, one-on-one consulting with the organizers on exercises and further verification projects.
  • +

- Organizers. + Organizers. (click on a name to see the bio)