Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Performance problem with Simpl and Isabelle si...


view this post on Zulip Email Gateway (Nov 01 2020 at 11:46):

From: Yulu Pan <pandaman@is.s.u-tokyo.ac.jp>
Dear all,

I am working on formal verification of Rust programs. I'm currently
embedding Rust's semantics into Isabelle/HOL using Schirmer's Simpl,
and while Simpl's Hoare logic and Verification Condition Generator are
great, they require much time and memory. I'm having trouble with the
performance, especially when combined with Isabelle's simplifier.

For example, the following theory models assignments through mutable references.
https://github.com/pandaman64/sabi/blob/eadb3640be4e9624a788702ea2b56c3c79b975fa/Rustv/Tests/ex/No_Alias_Precise.thy
My Windows box is AMD Ryzen 5 2600 with 32GB RAM, though the VCG on
line 30 takes a few minutes, and the subsequent (auto simp: Let_def)
takes even longer... If I give complex postconditions, like line 36,
the ML process consumes more than 24GB of memory, and an OutOfMemory
exception is recorded in the log of the jEdit session (so I could not
continue the process).

I would like to hear if there are any chips to improve performance.
I'd also like to hear about other formal verification frameworks for
imperative programming languages than Simpl. Is it feature-rich? Or
will it perform well?

Kind Regards,
Yulu


Last updated: Sep 28 2021 at 20:18 UTC