Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Work
:::info
Author:
(1) David S. Hardin, Cedar Rapids, IA USA [email protected].
:::
Table of Links
Abstract and Introduction
Dancing Links
The Rust Programming Language
RAC: Hardware/Software Co-Assurance at Scale
Rust and RAR
Dancing Links in Rust
Related Work
Conclusion, Acknowledgments, and References
7 Related Work
A number of domain-specific languages targeting both hardware and software realization, and providing support for formal verification, have been created. Cryptol [5], for example, has been employed as a “golden spec” for the evaluation of cryptographic implementations, in which automated tools perform equivalence checking between the Cryptol spec for a given algorithm, and the VHDL implementation.
\
Formal verification systems for Rust include Creusot [8], based on WhyML; Prusti [3], based on the Viper verification toolchain; and RustHorn [20], based on constrained Horn clauses. AWS is developing a model-checker for Rust, Kani [2]. Additionally, Carnegie-Mellon University is developing Verus, an SMT-based tool for formally verifying Rust programs [19]. With Verus, programmers express proofs and specifications using Rust syntax, allowing proofs to take advantage of Rust’s linear types and borrow checking. It will be interesting to attempt the sorts of correctness proofs achievable on our system using these verification tools
\
:::info
This paper is available on arxiv under CC 4.0 license.
:::
\
Welcome to Billionaire Club Co LLC, your gateway to a brand-new social media experience! Sign up today and dive into over 10,000 fresh daily articles and videos curated just for your enjoyment. Enjoy the ad free experience, unlimited content interactions, and get that coveted blue check verification—all for just $1 a month!
Account Frozen
Your account is frozen. You can still view content but cannot interact with it.
Please go to your settings to update your account status.
Open Profile Settings