paint-brush
Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Workby@gitflow
266 reads

Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Work

tldt arrow

Too Long; Didn't Read

In this paper, researchers describe an implementation of the Dancing Links optimization in the Rust programming language.
featured image - Verification of a Rust Implementation of Knuth’s Dancing
Links Using ACL2: Related Work
What is GitFlow? The Collaborative Git Alternative HackerNoon profile picture

Author:

(1) David S. Hardin, Cedar Rapids, IA USA [email protected].

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


This paper is available on arxiv under CC 4.0 license.