some more details

verus-lang · Oct 2, 2024 · a4f0c81 · a4f0c81
1 parent 5d45c70
commit a4f0c81
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 6 deletions.
diff --git 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,16 +126,22 @@ 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;
 }
 ul.organizers summary {
   cursor: pointer;
 }
+
diff --git a/pages/2024-sosp/index.html b/pages/2024-sosp/index.html
@@ -37,8 +37,8 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <span cl
           providing a much stronger guarantee than traditional testing.
           Instead of writing tests, the developer's effort towards correctness is focused on explaining
           why the implementation is correct, in the form of proof annotations.
-          These techniques can help Systems Researchers build reliable, secure systems, with less
-          reliance on runtime checking, which can be expensive.</p>
+          <span class="highlight">These techniques can help Systems Researchers build reliable, secure systems, with less
+            reliance on runtime checking, which can be expensive.</span></p>
 
           <p>This tutorial introduces <span class="highlight-2">Verus, an open-source,
           Rust-based verification tool designed specifically for systems software.
@@ -70,12 +70,13 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <span cl
             to no background in verification: we will start from simple Rust programs that the attendees will
             verify with the help of the organizers, and we will progressively move to more complex examples that
             introduce the core concepts necessary to get started in systems verification with Verus.
+          </p>
 
-            <span class="highlight-1">The morning program is designed to be self-contained. In the afternoon,
+          <p><span class="highlight">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.</span>
+            exercises presented in the morning with the help of the organizers.</span></p>
 
-            Morning Program (subject to change):
+          <p class="highlight-0">Morning Program (tentative):</p>
             <ul>
               <li>Overview of uses of verification, and introduction to systems verification;</li>
               <li>Verus set up: how to run it and where to find documentation;</li>
@@ -84,6 +85,7 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <span cl
               <li>Primers on "quantifiers" (∀/∃), how they are used in specifications and proofs (with interactive exercise);</li>
               <li>Primer on SMT solvers (underlying Verus' automation);</li>
               <li>"Capstone" interactive exercise to complete with the help of the organizers.</li>
+            </ul>
           </p>
 
           <p class="text">
@@ -94,16 +96,18 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <span cl
             programs with shared-memory concurrency, while letting attendees continue to build up their
             verification skills on a harder set of exercises.
 
+          <p class="highlight-0">Afternoon Program (tentative):</p>
             <ul>
               <li>How to debug a failing proof;</li>
               <li>Verifying code with unsafe pointers (with interactive exercise);</li>
               <li>Primer on Verus' mode system (for specification, proof, and executable code);</li>
               <li>Verifying shared-memory concurrent code with VerusSync (with interactive exercise);</li>
               <li>Open Q&amp;A, one-on-one consulting with the organizers on exercises and further verification projects.</li>
+            </ul>
           </p>
         </div>
         <div class="main relative card">
-          <span class="highlight">Organizers.</span>
+          <span class="highlight">Organizers.</span> (click on a name to see the bio)
 
           <ul class="organizers">
             <li>