BCVerifier
rev.650 (2013-03-13)
Choose an example
Cell example
Callback example
Callback example (alt.1)
Callback example (alt.2)
CallbackLock example
Awkward example (static)
Awkward example
NameGen example
NameGen example (alt.1)
OBool example
OBool example (alt.1)
OBool example (alt.2)
OBool example (alt.3)
Subtypes example
Subtypes example (alt.1)
OneOffLoop example
OneOffLoop example (alt.1)
Cubes example
Divergence example
Divergence example (alt)
Termination example
ComplexPlaces example
ObservableList example
ObservableList (iterators)
Old library implementation:
New library implementation:
package cell; public class Cell<T> { private T c; public void set(T o) {c = o;} public T get() {return c;} }
+
-
package cell; public class Cell<T> { private T c1, c2; private boolean f; public void set(T o) { f = !f; if(f) c1 = o; else c2 = o; } public T get(){ if(f) return c1; else return c2; } }
+
-
Coupling invariant:
invariant forall old Cell o1, new Cell o2 :: o1 ~ o2 ==> if o2.f then o1.c ~ o2.c1 else o1.c ~ o2.c2;
NONE
TYPECHECK
VERIFY
Specifies Boogie action after generation (one of [NONE, TYPECHECK, VERIFY])
Cap for sound program unrolling
Time limit in seconds to run prover (0 is unlimited)
Disable null checks to field accesses and method calls as well as !=0 checks to division/modulo
Check source compatibility
Number of stack splices to consider on stack (0 is unlimited)
Options
Verification in progress
