Email Gateway (Apr 23 2025 at 11:21): Email Gateway (Apr 23 2025 at 11:21):From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
We are excited to announce the release of AutoCorrode, an Isabelle/HOL framework for reasoning about imperative programs. AutoCorrode's core is language-agnostic, but as a driving example we are releasing AutoCorrode with a frontend for a Rust dialect which we call µRust. Functional specifications in AutoCorrode are written in separation logic, and we provide highly-configurable and scalable tactics for discharging weakest precondition proofs. AutoCorrode also includes representation-agnostic interfaces for reasoning about mutable state, as well efficiently executable implementations thereof and a "meta frame rule" to combine them.
AutoCorrode is available on https://github.com/awslabs/autocorrode. See the README for brief descriptions of its sessions, and Micro_Rust_Examples/Showcase.thy for introductory examples.
Best,
The AutoCorrode Team
(Hanno Becker
Nathan Chong,
Robert Dockins,
Jim Grundy,
Jason Z. S. Hu,
Ike Mulder,
Dominic P. Mulligan,
Paul Mure,
Lawrence C. Paulson,
Konrad Slind)
Last updated: May 06 2025 at 08:28 UTC