From 2093e434be77e9632c8fa900e83c7635d74d86d3 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 3 Oct 2024 16:57:16 +0200 Subject: [PATCH] Verus' -> Verus's --- pages/2024-sosp/index.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pages/2024-sosp/index.html b/pages/2024-sosp/index.html index 9b9bd5f..025aaed 100644 --- a/pages/2024-sosp/index.html +++ b/pages/2024-sosp/index.html @@ -55,7 +55,7 @@

Tutorial: Verifying Rust code with 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 @@ -88,7 +88,7 @@

Tutorial: Verifying Rust code with Verifying simple functions with pre- and post-conditions (with hands-on exercise);
  • Verifying programs with loops using loop invariants (with hands-on exercise);
  • Primers on "quantifiers" (∀/∃), how they are used in specifications and proofs (with hands-on exercise);
  • -
  • Primer on SMT solvers (underlying Verus' automation);
  • +
  • Primer on SMT solvers (underlying Verus's automation);
  • "Capstone" hands-on exercise to complete with the help of the organizers.
  • @@ -105,7 +105,7 @@

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