Verus: A Practical Foundation for Systems Verification
Formal verification is a promising approach to eliminate bugs at compile time, before they ship. Indeed, our community has verified a wide variety of system software. However, much of this success has required heroic developer effort, relied on bespoke logics for individual domains, or sacrificed expressiveness for powerful proof automation.
Authors
- Matthias Brun (ORCID: https://orcid.org/0009-0004-5349-4347)
- Tej Chajed (ORCID: https://orcid.org/0000-0002-9889-4828)
- Andrea Lattuada (ORCID: https://orcid.org/0000-0002-9303-452X)
- Chris Hawblitzel (ORCID: https://orcid.org/0000-0002-5676-0362)
- Travis Hance (ORCID: https://orcid.org/0009-0003-1104-7795)
- Chanhee Cho (ORCID: https://orcid.org/0009-0009-6620-9070)
- Jon Howell (ORCID: https://orcid.org/0000-0002-1781-2473)
- Jay Bosamiya (ORCID: https://orcid.org/0000-0002-5596-6828)
- P. Srinivasan
- Hayley LeBlanc (ORCID: https://orcid.org/0000-0003-3680-496X)
- Bryan Parno (ORCID: https://orcid.org/0000-0002-9113-1684)
- Jacob R. Lorch (ORCID: https://orcid.org/0000-0002-7269-2769)
- Oded Padon (ORCID: https://orcid.org/0009-0006-4209-1635)
- Reto Achermann (ORCID: https://orcid.org/0000-0003-3263-7236)
Institutions
- Microsoft (United States) (US)
- University of Wisconsin–Madison (US)
- University of Michigan (US)
- ETH Zurich (CH)
- Bellevue Hospital Center (US)
- Weizmann Institute of Science (IL)
- Carnegie Mellon University (US)
- The University of Texas at Austin (US)
Publication Details
- Published
- 2024-11-04
- DOI
- https://doi.org/10.1145/3694715.3695952
- Citations
- 20
- Primary Topic
- Security and Verification in Computing
- Type
- article
- Field-Weighted Citation Impact
- 6.95