Skip to content

Commit

Permalink
Verus' -> Verus's
Browse files Browse the repository at this point in the history
  • Loading branch information
utaal committed Oct 3, 2024
1 parent d0b2e23 commit 2093e43
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions pages/2024-sosp/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <a href=
<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.
It will then introduce Verus's 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
Expand Down Expand Up @@ -88,7 +88,7 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <a href=
<li>Verifying simple functions with pre- and post-conditions (with hands-on exercise);</li>
<li>Verifying programs with loops using loop invariants (with hands-on exercise);</li>
<li>Primers on "quantifiers" (∀/∃), how they are used in specifications and proofs (with hands-on exercise);</li>
<li>Primer on SMT solvers (underlying Verus' automation);</li>
<li>Primer on SMT solvers (underlying Verus's automation);</li>
<li>"Capstone" hands-on exercise to complete with the help of the organizers.</li>
</ul>
</p>
Expand All @@ -105,7 +105,7 @@ <h1><span class="highlight-2">Tutorial</span>: Verifying Rust code with <a href=
<ul>
<li>How to debug a failing proof;</li>
<li>Verifying code with unsafe pointers (with hands-on exercise);</li>
<li>Primer on Verus' mode system (for specification, proof, and executable code);</li>
<li>Primer on Verus's mode system (for specification, proof, and executable code);</li>
<li>Verifying shared-memory concurrent code with VerusSync (with hands-on exercise);</li>
<li>Open Q&amp;A, one-on-one consulting with the organizers on exercises and further verification projects.</li>
</ul>
Expand Down

0 comments on commit 2093e43

Please sign in to comment.