Email Gateway (Aug 22 2022 at 13:33): Email Gateway (Aug 22 2022 at 13:33):From: Станислав Владимирович Моисе ев <stanislav.moiseev@gmail.com>
Hello,
I'm working on a verification of properties of a large set containing
approximately 2 million objects. Each object is relatively simple.
These objects were constructed by a computer program; now I want to prove
that the result of the program is correct.
My plan is
1. to define 2 million objects.
2. to prove properties of every object (that is I need 2 million lemmas).
Each lemma has <=500 steps, each step is relatively simple. That is, I need
approx. 500*2mln = 1billion simple steps.
I'm going to generate the proofs for all that lemmas by another computer
programs.
Has anybody worked with specifications of this size?
Is it practical to conduct a proof of this size in Isabelle/HOL? If yes,
can you recommend how to organize the proof? If no, can you suggest other
verification tools?
My experiments show that it is impractical to define a set of 2 million
objects in Isabelle/HOL (Isabelle allocates a lot of memory and the
computation time is large).
I found that many small-size definitions are easier to handle than one
large definition. E.g. I was able to define 20 000 sets a1,...,a20000
containing 100 elements and then define 200 sets b1,...,b200 (each being a
union of 100 sets a_{100i+1},...,a_{100i+200}), and finally define a set
C as a union of b1,...,b200. But for aesthetic reasons I don't like it.
Moreover, given the speed of Isabelle, I'm not sure that proofs of 2
million lemmas can be conducted in a reasonable time (say, less than two
months).
Any ideas?
Stanislav.
Last updated: Apr 25 2024 at 08:20 UTC