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

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

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

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 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) Special Interest Group on Operating Systems (SIGOPS), 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.