IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
When using attribute method = mc with bit vector types (of any length), IVy claims correctness of the arguments n > n and n < n as if they were written n >= n and n <= n, respectively. This has been our observation on values from 0 to 31, including in the following small example.
#lang ivy1.7
attribute method = mc
type number
interpret number -> bv[4]
var test : number
after init {
test := 1;
}
invariant test < 1
When verified using ivy_check, the above model passes all checks.
When using
attribute method = mcwith bit vector types (of any length), IVy claims correctness of the argumentsn > nandn < nas if they were writtenn >= nandn <= n, respectively. This has been our observation on values from 0 to 31, including in the following small example.When verified using
ivy_check, the above model passes all checks.