Static verification made easy by fractional ownership!
Choose a sample code negative-tests/2cfa-test-real.imp negative-tests/arrays/array_list_BAD.e-imp negative-tests/arrays/array_list_BAD.imp negative-tests/arrays/array_rec_BAD.imp negative-tests/arrays/array_rec_overrun.imp negative-tests/arrays/silly_list_BAD.ch-imp negative-tests/arrays/silly_list_BAD2.ch-imp negative-tests/arrays/simple_BAD.imp negative-tests/arrays/simple_bad_len.imp negative-tests/arrays/simple_oob.imp negative-tests/arrays/simple_oob_nondet.imp negative-tests/bad-alias.imp negative-tests/challenge-problem/array_list_BAD.imp negative-tests/example-6-bad.imp negative-tests/example-6-bad2.imp negative-tests/gen-ref1-missing-alias.imp negative-tests/havoc-writes.imp negative-tests/incompleteness/conditional-aliasing.imp negative-tests/incompleteness/fermats.imp negative-tests/incompleteness/memory-relation.imp negative-tests/intro2_BAD.imp negative-tests/nullity-checking.imp negative-tests/nullity/null-prop.imp negative-tests/nullity/trivial.imp negative-tests/recursive-tests/bad_subtyping.imp negative-tests/recursive-tests/havoc_alias.imp negative-tests/recursive-tests/havoc_deref.imp negative-tests/recursive-tests/incr_list_BAD.imp negative-tests/recursive-tests/pointer-unfolding.imp negative-tests/recursive-tests/simple-list_BAD.imp negative-tests/recursive-tests/sorted-list-BAD1.imp negative-tests/recursive-tests/sorted-list-BAD2.imp negative-tests/recursive-tests/sorted-list-BAD3.imp negative-tests/recursive-tests/sorted-list-test-nondet-BAD1.imp negative-tests/recursive-tests/sorted-list-test-nondet-BAD2.imp negative-tests/recursive-tests/sorted-list-test-nondet-BAD3.imp negative-tests/recursive-tests/trivial_BAD.imp negative-tests/shuffle-in-call.imp negative-tests/simple-bad.imp negative-tests/swapping_BAD.imp positive-tests/2cfa/2cfa-nondet.imp positive-tests/2cfa/2cfa-test-real.imp positive-tests/2cfa/2cfa-test.imp positive-tests/arrays/array_alias.imp positive-tests/arrays/array_copy.imp positive-tests/arrays/array_list.imp positive-tests/arrays/array_list_loop.imp positive-tests/arrays/array_rec.imp positive-tests/arrays/silly_list.ch-imp positive-tests/arrays/simple.imp positive-tests/assume-zero.imp positive-tests/assume_positive.imp positive-tests/assume_positive_ref.imp positive-tests/challenge-problem/array_list.imp positive-tests/challenge-problem/array_list_direct.imp positive-tests/challenge-problem/array_list_nd.imp positive-tests/challenge-problem/array_list_nd_tight.imp positive-tests/challenge-problem/array_list_tight.imp positive-tests/challenge-problem/array_list_trunc.imp positive-tests/challenge-problem/data.org positive-tests/challenge-problem/direct-encoding.smt positive-tests/compare.imp positive-tests/complex_op.imp positive-tests/conjoin.imp positive-tests/contents.imp positive-tests/dep-tuple.imp positive-tests/example-1.imp positive-tests/example-3.imp positive-tests/example-4.imp positive-tests/example-5.imp positive-tests/example-6-typable.imp positive-tests/flow-sensitive-example.imp positive-tests/gamma.imp positive-tests/gen-ref1.imp positive-tests/gen-ref2.imp positive-tests/inline_assume.imp positive-tests/intro-example-old.imp positive-tests/intro-fig1.imp positive-tests/intro-fig2.imp positive-tests/intro2.imp positive-tests/jayhorn/false_negative.imp positive-tests/jayhorn/linger_dec.imp positive-tests/jayhorn/loop-simple.imp positive-tests/jayhorn/paper-example.imp positive-tests/jayhorn/rec_simple.imp positive-tests/maybe-null.imp positive-tests/min-int.imp positive-tests/min-pointer.imp positive-tests/multi-assign.imp positive-tests/nested-pointer.imp positive-tests/nested-tup.imp positive-tests/null-prop.imp positive-tests/nullity-tracking.imp positive-tests/nullity/null-prop.imp positive-tests/nullity/nullity-checking.imp positive-tests/pre-relation/idem.imp positive-tests/pre-relation/in_place.imp positive-tests/pre-relation/insert_val.imp positive-tests/pre-relation/insert_val_rel.imp positive-tests/propagate.imp positive-tests/ptr.imp positive-tests/push-pull-decr.imp positive-tests/push-pull-rich.imp positive-tests/push-pull.imp positive-tests/reachability.imp positive-tests/recursive-direct.imp positive-tests/recursive-tests/append-list.imp positive-tests/recursive-tests/incr_list.imp positive-tests/recursive-tests/partial_havoc.imp positive-tests/recursive-tests/prepend-list.imp positive-tests/recursive-tests/silly-list.imp positive-tests/recursive-tests/simple-list-nondet.imp positive-tests/recursive-tests/simple-list.imp positive-tests/recursive-tests/sorted-list-decr.imp positive-tests/recursive-tests/sorted-list-test-nondet.imp positive-tests/recursive-tests/sorted-list-test.imp positive-tests/recursive-tests/sorted-list-tup.imp positive-tests/recursive-tests/stable_alias.imp positive-tests/recursive-tests/trivial.imp positive-tests/recursive.imp positive-tests/relation-ptr.imp positive-tests/relation.imp positive-tests/relational-param.imp positive-tests/remove.imp positive-tests/runtime_proof.imp positive-tests/runtime_proof_indirect.imp positive-tests/simple-alias.imp positive-tests/simple_addition.imp positive-tests/simple_addition2.imp positive-tests/simple_pointer.imp positive-tests/singleton_tuple.imp positive-tests/subalias.imp positive-tests/swapping.imp positive-tests/tautology.imp positive-tests/trivial-assume.imp positive-tests/tuple-alias.imp positive-tests/tuple-rel-2.imp positive-tests/tuple-rel.imp
Check
About ConSORT - Static assertion checker for heap-manipulating programs
ConSORT is a static assertion cheker for a simple imperative language for heap-manipulating programs. The underlying theory is based on the combination of fractional ownership and refinement types.
Project Home