Future Work in Rust Co-Assurance

22 Jan 2025

Explore the latest advancements in Rust-based toolchains for hardware/software co-assurance.

Proving Theorems for Rust’s Dancing Links in ACL2

22 Jan 2025

Explore how 160 theorems, including correctness proofs for CDLLs, validate Rust's Dancing Links implementation using ACL2’s automated verification tools.

Machine-Generated Code That Works

22 Jan 2025

Discover how RAR Rust source is translated into ACL2 with Plexi, ensuring readable, high-assurance machine-generated code for robust formal reasoning.

Simplifying Circular Data Structures with Rust’s RAR Subset

22 Jan 2025

Learn how Knuth’s Dancing Links optimization works in Rust’s RAR subset with array-based circular doubly-linked lists for efficient high-assurance systems.

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast

21 Jan 2025

Discover how Rust and ACL2 optimize Dancing Links for exact cover problems like Sudoku, leveraging memory safety and efficient list manipulation.

The Case for Rust Programming as a Game-Changer for High-Level Synthesis

21 Jan 2025

Discover how Rust and RAR enable memory-safe, high-assurance hardware/software co-design, with applications from cryptography to autonomous systems.

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C

21 Jan 2025

Explore how Restricted Algorithmic C and ACL2 enable scalable hardware/software co-assurance with formal verification for critical system designs.

RRR—Rust, RAR, and RAC: The Trifecta for Co-Design Excellence

21 Jan 2025

Restricted Algorithmic Rust (RAR), a subset of Rust enables high-assurance designs by integrating with RAC, leveraging Rust’s safety features for co-design.