H Becker of AWS announces AutoCorrode (https://github.com/awslabs/AutoCorrode/), an Isabelle/HOL framework for reasoning about imperative programs and with a frontend for a Rust dialect which we call µRust. Functional specifications in AutoCorrode are written in separation logic.
Comments