add more to SOSP turorial website

pages/2024-sosp/index.html

@@ -29,30 +29,33 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <span cl
           </p>
         </div>
         <div class="main relative card">
-          <p class="text">
-            Software verification can prove that 
-            a program will behave correctly for all possible inputs it might receive;
-            hence it provides much stronger guarantees than traditional testing.
-            This tutorial introduces Verus,
-            an open-source, Rust-based verification tool designed specifically for systems software.
-            <span class="highlight">Verus aims to provide efficient proof automation
-            and scale to large, complex systems,
-            and it is developed by a community of academic and industry contributors.</span>
-          </p>
+          <p class="text">Good engineers love well-written tests because they confirm that the code works correctly,
+          at least for the tested inputs. What if you could check every possible input?</p>
+
+          <p class="text">In software verification, tests are replaced by a complete specification; the verifier provides
+          a compile-time check that the implementation matches the spec,
+          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>
+
+          <p>This tutorial introduces <span class="highlight-2">Verus, an open-source,
+          Rust-based verification tool designed specifically for systems software.
+          Verus provides efficient proof automation and scales to large, complex systems.</span>
+          Verus is developed by a community of academic and industry contributors,
+          it is already seeing industrial application at Microsoft and Amazon,
+          and two of three best papers at OSDI 2024 are built on Verus.</p>
+
+          <p>This tutorial will briefly introduce the state-of-the art in software verification,
+          covering the benefits and challenges of verification as an engineering methodology,
+          especially with regards to systems software.
+          It will then introduce Verus' basic features with a set of interactive exercises.
+          No prior knowledge of Rust is required beyond familiarity with C-like languages.
+          The tutorial will then move on to verification principles, and Verus techniques necessary
+          to verify complex systems involving
+          <span class="higlight">complex data structures, network communication, and shared-memory concurrency</span>.
 
-          <p class="text">
-            This tutorial will briefly introduce the state-of-the art in software verification,
-            covering the  benefits and challenges of verification as an engineering methodology, 
-            especially with regards to systems software.
-            It will then introduce Verus's basic features 
-            (without requiring prior knowledge of Rust,
-            other than familiarity with C-like langugages)
-            with a set of interactive exercises.
-            Building on this foundation, 
-            the tutorial will then introduce concepts necessary to verify more complex systems, 
-            such as those relying on complex data structures, network communication, or shared-memory
-            concurrency.
-          <p>
         </div>
         <div class="main relative card">
           <p class="text">
@@ -67,15 +70,36 @@ <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.
+
+            <span class="highlight-1">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>
+
+            Morning Program (subject to change):
+            <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>
+              <li>Verifying simple functions with pre- and post-conditions (with interactive exercise);</li>
+              <li>Verifying programs with loops using loop invariants (with interactive exercise);</li>
+              <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>
           </p>
 
           <p class="text">
             <span class="highlight-2">Afternoon.</span>
             In the second half of the day, we will continue by building up to more complex systems, protocols,
             and verification tasks. This will be done in a way that allows attendees already familiar with verification
             to get exposure to the more advanced Verus features, such as support for verifying the correctness of
-            programs with shared-memory concurrency, while letting less experienced attendees continue to build up their
+            programs with shared-memory concurrency, while letting attendees continue to build up their
             verification skills on a harder set of exercises.
+
+            <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>
           </p>
         </div>
         <div class="main relative card">