search

kenmcmil / ivy

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.
Other
77 stars 24 forks source link

Bounded Verification Feature #47

Closed TonyZhangND closed 2 years ago

TonyZhangND commented 2 years ago

Section 2.2 of the PLDI'16 paper describes a model checking functionality ion Ivy to rule out some protocol bugs before the inductive invariant search phase. However, I can't find any commands to do this bounded model checking. Is this feature still available?

nano-o commented 2 years ago

If I remember correctly, you have to add attribute method=bmc[3] (for a bound of 3 transitions) to the isolate you want to check.

TonyZhangND commented 2 years ago

Thank you, that worked!