Verus: A Practical Foundation for Systems Verification
Authors: 
Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, Bryan ParnoAuthors Info & Claims
Pages 438 - 454
Abstract
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.
Building on prior work on Verus, we aim to enable faster, cheaper verification of rich properties for realistic systems. We do so by integrating and optimizing the best choices from prior systems, tuning our design to overcome barriers encountered in those systems, and introducing novel techniques.
We evaluate Verus's effectiveness with a wide variety of case-study systems, including distributed systems, an OS page table, a library for NUMA-aware concurrent data structure replication, a crash-safe storage system, and a concurrent memory allocator, together comprising 6.1K lines of implementation and 31K lines of proof. Verus verifies code 3--61× faster and with less effort than the state of the art.
Our results suggest that Verus offers a platform for exploring the next frontiers in system-verification research. Because Verus builds on Rust, Verus is also positioned for wider use in production by developers who have already adopted Rust in the pursuit of more robust systems.
Supplemental Material
External - Case Studies and Reproducible Experiments for Verus: A Practical Foundation for Systems Verification
The artifact repository for the paper "Verus: A Practical Foundation for Systems Verification". It contains links to the verification case studies of systems software used to evaluate Verus, the sources for additional benchmarks of Verus and other verification tools, a guide on how to reproduce the results in the paper, and the scripts and packages necessary to reproduce the results.
Download from: https://github.com/verus-lang/paper-sosp24-artifact
References
[1]
Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-button verification of file systems via crash refinement. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), November 2016.
[2]
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using Crash Hoare Logic for certifying the FSCQ file system. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2015.
[3]
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying concurrent, crash-safe systems with Perennial. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2019.
[4]
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2017.
[5]
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2019.
[6]
Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), November 2020.
[7]
Oded Padon, Kenneth L. McMillan, Mooly Sagiv, Aurojit Panda, and Sharon Shoham. Ivy: Safety verification by interactive generalization. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), 2016.
[8]
Kenneth L. McMillan and Oded Padon. Ivy: A multi-modal verification tool for distributed algorithms. In Proceedings of the Conference on Computer Aided Verification (CAV), 2020.
[9]
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. Modularity for decidability of deductive verification with applications to distributed systems. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), 2018.
[10]
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. In Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), December 2023.
[11]
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. VCC: A practical system for verifying concurrent C. In Proceedings of the Conference on Theorem Proving in Higher Order Logics, 2009.
[12]
Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), October 2014.
[13]
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet: Proving practical distributed systems correct. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2015.
[14]
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cedric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, and Santiago Zanella-Beguelin. EverCrypt: A fast, verified, cross-platform cryptographic provider. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland), May 2020.
[15]
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, and Santiago Zanella-Béguelin. HACL×N: Verified generic SIMD crypto (for all your favorite platforms). In Proceedings of the ACM Conference on Computer and Communications Security (CCS), October 2020.
[16]
Travis Hance, Andrea Lattuada, C. Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. Storage systems are distributed systems (so verify them that way!). In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2020.
[17]
R. Piskac, L. M. de Moura, and N. Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. Journal of Automated Reasoning, 44(4), 2010.
[18]
Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. Paxos made EPR: Decidable reasoning about distributed protocols. In Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), October 2017.
[19]
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A. Sakallah. I4: Incremental inference of inductive invariants for verification of distributed protocols. In Proceedings of the ACM Symposium on Operating Systems Principles, (SOSP), 2019.
[20]
Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. Finding invariants of distributed systems: It's a small (enough) world after all. In Proceedings of the USENIX Symposium on Networked Systems Design and Implementation (NSDI), April 2021.
[21]
Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2022.
[22]
Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. DistAI: Data-Driven automated invariant learning for distributed protocols. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2021.
[23]
The Verus Contributors. Verus repository. https://github.com/verus-lang/verus.
[24]
Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jay Lorch, Oded Padon, and Bryan Parno. Verus SOSP artifact. https://verus-lang.github.io/papersosp24-artifact/, 2024.
[25]
Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. Anvil: Verifying liveness of cluster management controllers. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2024.
[26]
Xiangdong Chen, Zhaofeng Li, Lukas Mesicek, Vikram Narayanan, and Anton Burtsev. Atmosphere: Towards practical verified kernels in Rust. In Proceedings of the Workshop on Kernel Isolation, Safety and Verification (KISV), 2023.
[27]
Ziqiao Zhou, Weiteng Chen, Chris Hawblitzel, and Weidong Cui. VeriSMo: A verified security module for confidential VMs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2024.
[28]
Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui. Leveraging large language models for automated proof synthesis in Rust. https://arxiv.org/abs/2311.03739, 2023.
[29]
Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. Sharding the state machine: Automated modular reasoning for complex concurrent systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2023.
[30]
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, Frans Kaashoek, and Nickolai Zeldovich. Grove: A separation-logic library for verifying distributed systems. In Proceedings of the Symposium on Operating Systems Principles (SOSP), 2023.
[31]
Coq Development Team. The Coq Proof Assistant https://coq.inria.fr/.
[32]
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover. In Proceedings of the Conference on Automated Deduction (CADE), August 2015.
[33]
John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the IEEE Symposium on Logic in Computer Science, 2002.
[34]
K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2010.
[35]
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F★. In Proceedings of the ACM Conference on Principles of Programming Languages (POPL), 2016.
[36]
Nicholas D. Matsakis and Felix S. Klock. The Rust language. Ada Lett., 34(3):103--104, October 2014.
[37]
Steve Klabnik and Carol Nichols. The Rust Programming Language. No Starch Press, USA, 2018.
[38]
Liam Proven. Linux 6.1: Rust to hit mainline kernel. https://www.theregister.com/2022/10/05/rust_kernel_pull_request_pulled/, October 2022.
[39]
Shane Miller and Carl Lerche. Sustainability with Rust. https://aws.amazon.com/blogs/opensource/sustainability-with-rust/, February 2022.
[40]
Google. Announcing KataOS and Sparrow. https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html, October 2022.
[41]
Yechan Bae, Youngsuk Kim, Ammar Askar, Jungwon Lim, and Taesoo Kim. RUDRA: Finding memory safety bugs in Rust at the ecosystem scale. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2021.
[42]
Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Haojun Ma, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao. Armada: Automated verification of concurrent code with sound semantic extensibility. ACM Transactions on Programming Languages and Systems, 44(2), June 2022.
[43]
Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), October 2017.
[44]
Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, and Bryan Parno. Mariposa: Measuring SMT instability in automated program verification. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference, October 2023.
[45]
Leslie Lamport. Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
[46]
L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008.
[47]
Robert Floyd. Assigning meanings to programs. In Proceedings of the Symposia in Applied Mathematics, 1967.
[48]
Tony Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12, 1969.
[49]
Michał Moskal. Programming with triggers. In Proceedings of the Workshop on Satisfiability Modulo Theories, 2009.
[50]
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Reducing liveness to safety in first-order logic. PACMPL, 2(POPL):26:1--26:33, 2018.
[51]
Jason R. Koenig, Oded Padon, Sharon Shoham, and Alex Aiken. Inferring invariants with quantifier alternations: Taming the search space explosion. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 13243, 2022.
[52]
Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Certified verification of algebraic properties on low-level mathematical constructs in cryptographic programs. In Proceedings of the ACM Conference on Computer and Communications Security (CCS), 2017.
[53]
Yi Zhou, Sydney Gibson, Sarah Cai, Menucha Winchell, and Bryan Parno. Galápagos: Developing verified low-level cryptography on heterogeneous hardwares. In Proceedings of the ACM Conference on Computer and Communications Security (CCS), November 2023.
[54]
Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Haojun Ma, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao. Armada code repository. https://github.com/microsoft/Armada/blob/ee799110f9aecc3deab31b94521bdbcd27f58363/Test/qbss/bv.dfy#L54, December 2023.
[55]
Martijn Oostdijk and Herman Geuvers. Proof by computation in the Coq system. Theoretical Computer Science, 272(1--2), February 2002.
[56]
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. Meta-F*: Proof automation with SMT, tactics, and metaprograms. In Proceedings of the European Symposium on Programming (ESOP), April 2019.
[57]
Ralf Jung, R. Krebbers, Jacques-Henri Jourdan, A. Bizjak, L. Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28, 2018.
[58]
Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1--3), April 2007.
[59]
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. Vale: Verifying high-performance cryptographic assembly code. In Proceedings of the USENIX Security Symposium, August 2017.
[60]
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. Verified low-level programming embedded in F*. PACMPL, 1(ICFP), September 2017.
[61]
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jiangyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, and Jean Karim Zinzindohoué. Implementing and proving the TLS 1.3 record layer. In Proceedings of the IEEE Symposium on Security and Privacy, May 2017.
[62]
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, and Yi Zhou. A security model and fully verified implementation for the IETF QUIC record layer. In Proceedings of the IEEE Symposium on Security and Privacy, May 2021.
[63]
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, and Karthikeyan Bhargavan. Formally verified cryptographic web applications in WebAssembly. In Proceedings of the IEEE Symposium on Security and Privacy, May 2019.
[64]
Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, and Alexander J. Summers. Modular specification and verification of closures in Rust. Proceedings of the ACM on Programming Languages, 5(OOPSLA), October 2021.
[65]
Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. Creusot: A foundry for the deductive verication of Rust programs. In Proceedings of the International Conference on Formal Engineering Methods, October 2022.
[66]
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Haojun Ma, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet code. https://research.microsoft.com/projects/ironclad/, 2015.
[67]
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel. Linear types for large-scale systems verification. In Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), November 2022.
[68]
Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai, and Gerd Zellweger. NrOS: Effective replication and sharing in an operating system. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2021.
[69]
Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. IronSync OSDI 2023 artifact. https://github.com/secure-foundations/ironsync-osdi2023, 2023.
[70]
Daan Leijen, Ben Zorn, and Leonardo de Moura. Mimalloc: Free list sharding in action. Technical Report MSR-TR-2019-18, Microsoft, June 2019.
[71]
Daan Leijen. Mimalloc-bench. https://github.com/daanx/mimalloc-bench, 2023.
[72]
Intel. Intel Optane persistent memory. https://www.intel.com/content/www/us/en/products/docs/memory-storage/optane-persistent-memory/overview.html.
[73]
Jian Xu, Lu Zhang, Amirsaman Memaripour, Akshatha Gangadharaiah, Amit Borase, Tamires Brito Da Silva, Steven Swanson, and Andy Rudoff. NOVA-Fortis: A fault-tolerant non-volatile main memory file system. In Proceedings of the ACM Symposium on Operating Systems Principles, (SOSP), 2017.
[74]
Linux Kernel Developers. Direct Access for files. https://www.kernel.org/doc/Documentation/filesystems/dax.txt.
[75]
PMDK Developers. libpmemlog. https://pmem.io/pmdk/manpages/linux/v1.3/libpmemlog.3/.
[76]
PMDK Developers. PMDK. https://pmem.io/pmdk/.
[77]
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), January 2014.
[78]
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1), 2014.
[79]
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM (CACM), 52(7):107--115, 2009.
[80]
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. Verdi: A framework for implementing and formally verifying distributed systems. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), June 2015.
[81]
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the USENIX Conference on Operating Systems Design and Implementation (OSDI), 2016.
[82]
Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. Spoq: Scaling machine-checkable systems verification in Coq. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI), July 2023.
[83]
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002.
[84]
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Michael Norrish, Rafal Kolanski, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2009.
[85]
Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. Cogent: Verifying high-assurance file system implementations. In Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016.
[86]
Philip Wadler. Linear types can change the world! In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods, 1990.
[87]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2(POPL), January 2018.
[88]
Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016.
[89]
Son Ho and Jonathan Protzenko. Aeneas: Rust verification by functional translation. Proceedings of the ACM on Programming Languages, 6(ICFP):711--741, 2022.
Index Terms
- Verus: A Practical Foundation for Systems Verification
Index terms have been assigned to the content through auto-classification.
Recommendations
Verus: Verifying Rust Programs using Linear Ghost Types
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such ...
Verus: a tool for quantitative analysis of finite-state real-time systems
Symbolic model checking is a technique for verifying finite-state concurrent systems. Models with up to 1030 states can often be verified in minutes. In this paper, we present a new tool to analyze real-time systems, based on this technique. We have ...
Automated verification of practical garbage collectors
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesGarbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
November 2024
765 pages
ISBN:9798400712517
DOI:10.1145/3694715
- Chair:
- Emmett Witchel,
- Co-chair:
- Christopher J Rossbach,
- Program Chair:
- Andrea Arpaci-Dusseau,
- Program Co-chair:
- Kimberly Keeton
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
- USENIX
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 November 2024
Check for updates
Badges
Qualifiers
- Research-article
Funding Sources
- NSF
- AFRL, DARPA
Conference
SOSP '24
Sponsor:
SOSP '24: ACM SIGOPS 30th Symposium on Operating Systems Principles
November 4 - 6, 2024
TX, Austin, USA
Acceptance Rates
SOSP '24 Paper Acceptance Rate 43 of 245 submissions, 18%;
Overall Acceptance Rate 174 of 961 submissions, 18%
Upcoming Conference
SOSP '25
- Sponsor:
- sigops
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 209Total Downloads
- Downloads (Last 12 months)209
- Downloads (Last 6 weeks)209
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in