- 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. - 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. -
+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?
+ +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.
+ +This tutorial introduces Verus, an open-source, + Rust-based verification tool designed specifically for systems software. + Verus provides efficient proof automation and scales to large, complex systems. + 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.
+ +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 + complex data structures, network communication, and shared-memory concurrency. -
- 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. -