Research team featuring CMU faculty, students wins SOSP 2024 Distinguished Artifact Award

A team of researchers featuring Carnegie Mellon University Opens in new window faculty, students, and alumni has received the 30th Symposium on Operating Systems Principles (SOSP) Distinguished Artifact Award Opens in new window for the paper Verus: A Practical Foundation for Systems Verification Opens in new window.

The team features CMU Ph.D. student Chanhee Cho Opens in new window; recent Ph.D. alumni Jay Bosamiya Opens in new window and Travis Hance Opens in new window; and Bryan Parno Opens in new window, Kavčić-Moura professor of Electrical and Computer Engineering Opens in new window and Computer Science Opens in new window.

It also includes Andrea Lattuada of MPI-SWS, Matthias Brun of ETH Zurich, Hayley LeBlanc of the University of Texas at Austin, Pranav Srinivasan of the University of Michigan, Reto Achermann of the University of British Columbia, Tej Chajed of the University of Wisconsin–Madison, Chris Hawblitzel of Microsoft Research, Jon Howell of VMWare Research, Jacob R. Lorch of Microsoft Research, and Oded Padon of the Weizmann Institute of Science.

“We were pleasantly surprised and honored to have our work highlighted by the award,” said Parno.

A scientific paper consists of a constellation of artifacts that extend beyond the document itself: software, hardware, evaluation data and documentation, raw survey results, mechanized proofs, models, test suites, benchmarks, and so on. In some cases, the quality of these artifacts is as important as that of the document itself.

SOSP’s optional artifact evaluation process considered the availability and functionality of artifacts associated with their corresponding papers, along with the reproducibility of the paper’s key results and claims with these artifacts. Artifact evaluation was single blind, and was conducted by the SOSP Artifact Evaluation Committee (AEC).

The goal of artifact evaluation is to incentivize authors to invest in their broader scientific community by producing artifacts that illustrate their claims, enable others to validate those claims, and accelerate future scientific progress by providing a platform for others to start from.

“Since Verus Opens in new window is relatively new, we wanted to evaluate it on many different kinds of complex systems software,” said Parno. “By making Verus itself, our verified case studies, and the evaluation scripts available and reusable, we make it easier for others to confirm our evaluation results and to build on our work. Our case studies also provide examples of how to use Verus at scale.”

Formal verification is a promising approach to eliminate bugs at compile time, before they ship. Historically, however, many successful formal verification efforts have required heroic developer effort, relied on bespoke logics for individual domains, or sacrificed expressiveness for powerful proof automation.

Building on their prior work on Verus, the research team aimed to enable faster, cheaper verification of rich properties for realistic systems. They did so by integrating and optimizing the best choices from prior systems, tuning their design to overcome barriers encountered in those systems, and introducing novel techniques.

“Our results indicate that Verus requires less effort than (and reports verification results far faster than) comparable prior tools. We’re excited to keep improving Verus and see what the broader community builds with it,” said Parno.

Sponsored by the Association of Computing Machinery (ACM) Opens in new window Special Interest Group on Operating Systems (SIGOPS) Opens in new window, SOSP is the world's premier forum for researchers, developers, programmers, and teachers of computer systems technology. Academic and industrial participants present research and experience papers that cover the full range of theory and practice of computer systems software.