On 10/03/2011 10:04 PM, Florian Haftmann wrote:
If you have strong feelings about this being at the wrong place, you can
move it.
I have no »feelings«, just an educated guess that sometimes somebody
*will* move it, either by necessity or by psychological strain. In an
amortized view, you do n
Hi Gerwin,
This is because by default the smt method tries to reconstruct the
proof of Z3. For bitvectors, however, there is currently no Z3 proof
reconstruction. You might want to invoke the smt method as an oracle:
lemma "(x :: 8 word) + x = 2 * x"
using [[smt_oracle]]
by smt
Chee
Am 05/10/2011 00:23, schrieb David Blubaugh:
> Has anyone ever developed a verified and validated version of the Linux
> kernel by utilizing the Isabelle / HOL environment ??
Not that I have heard about it ;-)
>
> Does Isabelle support non-determinsitic model checking as well as
> theorem prov
I'm getting
lemma "(x :: 8 word) + x = 2 * x"
apply smt
Solver z3: Z3 proof parser (line 2): unknown sort: "bv"
I was trying remote Z3 from a Mac.
This is on isabelle 20b3377b08d7, but I don't think anything relevant has
changed since Sep 26.
Am I doing something wrong? Sounds like Z3 res
Has anyone ever developed a verified and validated version of the Linux kernel
by utilizing the Isabelle / HOL environment ??
Would anybody be interested in developing such a kernel ??
Does Isabelle support non-determinsitic model checking as well as theorem
proving of software system
