GitHub - chc-comp/rust-horn: Benchmarks generated by RustHorn from verifying small rust programs

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 1 Commit
README.md		README.md
bmc-1-test-bmc-1-safe.smt2		bmc-1-test-bmc-1-safe.smt2
bmc-1-test-bmc-1-unsafe.smt2		bmc-1-test-bmc-1-unsafe.smt2
bmc-2-test-bmc-2-safe.smt2		bmc-2-test-bmc-2-safe.smt2
bmc-2-test-bmc-2-unsafe.smt2		bmc-2-test-bmc-2-unsafe.smt2
bmc-3-test-bmc-3-safe.smt2		bmc-3-test-bmc-3-safe.smt2
bmc-3-test-bmc-3-unsafe.smt2		bmc-3-test-bmc-3-unsafe.smt2
bmc-4-test-bmc-diamond-1-safe.smt2		bmc-4-test-bmc-diamond-1-safe.smt2
bmc-4-test-bmc-diamond-1-unsafe.smt2		bmc-4-test-bmc-diamond-1-unsafe.smt2
bmc-5-test-bmc-diamond-2-safe.smt2		bmc-5-test-bmc-diamond-2-safe.smt2
bmc-5-test-bmc-diamond-2-unsafe.smt2		bmc-5-test-bmc-diamond-2-unsafe.smt2
inc-max-1-base-safe.smt2		inc-max-1-base-safe.smt2
inc-max-1-base-unsafe.smt2		inc-max-1-base-unsafe.smt2
inc-max-2-base3-safe.smt2		inc-max-2-base3-safe.smt2
inc-max-2-base3-unsafe.smt2		inc-max-2-base3-unsafe.smt2
inc-max-3-repeat-safe.smt2		inc-max-3-repeat-safe.smt2
inc-max-3-repeat-unsafe.smt2		inc-max-3-repeat-unsafe.smt2
inc-max-4-repeat3-safe.smt2		inc-max-4-repeat3-safe.smt2
inc-max-4-repeat3-unsafe.smt2		inc-max-4-repeat3-unsafe.smt2
just-rec-1-base-safe.smt2		just-rec-1-base-safe.smt2
just-rec-1-base-unsafe.smt2		just-rec-1-base-unsafe.smt2
linger-dec-1-basic-safe.smt2		linger-dec-1-basic-safe.smt2
linger-dec-1-basic-unsafe.smt2		linger-dec-1-basic-unsafe.smt2
linger-dec-2-basic3-safe.smt2		linger-dec-2-basic3-safe.smt2
linger-dec-2-basic3-unsafe.smt2		linger-dec-2-basic3-unsafe.smt2
linger-dec-3-exact-safe.smt2		linger-dec-3-exact-safe.smt2
linger-dec-3-exact-unsafe.smt2		linger-dec-3-exact-unsafe.smt2
linger-dec-4-exact3-safe.smt2		linger-dec-4-exact3-safe.smt2
linger-dec-4-exact3-unsafe.smt2		linger-dec-4-exact3-unsafe.smt2
lists-1-append-safe.smt2		lists-1-append-safe.smt2
lists-1-append-unsafe.smt2		lists-1-append-unsafe.smt2
lists-2-inc-all-safe.smt2		lists-2-inc-all-safe.smt2
lists-2-inc-all-unsafe.smt2		lists-2-inc-all-unsafe.smt2
lists-3-inc-some-safe.smt2		lists-3-inc-some-safe.smt2
lists-3-inc-some-unsafe.smt2		lists-3-inc-some-unsafe.smt2
lists-4-inc-some2-safe.smt2		lists-4-inc-some2-safe.smt2
lists-4-inc-some2-unsafe.smt2		lists-4-inc-some2-unsafe.smt2
prusti-1-pass-rosetta-Ackermann_function-base.smt2		prusti-1-pass-rosetta-Ackermann_function-base.smt2
prusti-2-pass-rosetta-Ackermann_function-same.smt2		prusti-2-pass-rosetta-Ackermann_function-same.smt2
prusti-3-pass-paper_examples-points-compress.smt2		prusti-3-pass-paper_examples-points-compress.smt2
prusti-4-pass-paper_examples-borrows_align.smt2		prusti-4-pass-paper_examples-borrows_align.smt2
prusti-5-pass-demos-account.smt2		prusti-5-pass-demos-account.smt2
prusti-6-fail-demos-account_error_1.smt2		prusti-6-fail-demos-account_error_1.smt2
prusti-7-pass-mut_borrows-restore.smt2		prusti-7-pass-mut_borrows-restore.smt2
simple-1-01_unsat.smt2		simple-1-01_unsat.smt2
simple-2-04_recursive_unsat.smt2		simple-2-04_recursive_unsat.smt2
simple-3-05_recursive_sat.smt2		simple-3-05_recursive_sat.smt2
simple-4-06_loop_unsat.smt2		simple-4-06_loop_unsat.smt2
simple-5-hhk2008.smt2		simple-5-hhk2008.smt2
simple-6-unique_scalar.smt2		simple-6-unique_scalar.smt2
swap-dec-1-base-safe.smt2		swap-dec-1-base-safe.smt2
swap-dec-1-base-unsafe.smt2		swap-dec-1-base-unsafe.smt2
swap-dec-2-base3-safe.smt2		swap-dec-2-base3-safe.smt2
swap-dec-2-base3-unsafe.smt2		swap-dec-2-base3-unsafe.smt2
swap-dec-3-exact-safe.smt2		swap-dec-3-exact-safe.smt2
swap-dec-3-exact-unsafe.smt2		swap-dec-3-exact-unsafe.smt2
swap-dec-4-exact3-safe.smt2		swap-dec-4-exact3-safe.smt2
swap-dec-4-exact3-unsafe.smt2		swap-dec-4-exact3-unsafe.smt2
swap2-dec-1-base-safe.smt2		swap2-dec-1-base-safe.smt2
swap2-dec-1-base-unsafe.smt2		swap2-dec-1-base-unsafe.smt2
swap2-dec-2-base3-safe.smt2		swap2-dec-2-base3-safe.smt2
swap2-dec-2-base3-unsafe.smt2		swap2-dec-2-base3-unsafe.smt2
swap2-dec-3-exact-safe.smt2		swap2-dec-3-exact-safe.smt2
swap2-dec-3-exact-unsafe.smt2		swap2-dec-3-exact-unsafe.smt2
swap2-dec-4-exact3-safe.smt2		swap2-dec-4-exact3-safe.smt2
swap2-dec-4-exact3-unsafe.smt2		swap2-dec-4-exact3-unsafe.smt2
trees-1-append-safe.smt2		trees-1-append-safe.smt2
trees-1-append-unsafe.smt2		trees-1-append-unsafe.smt2
trees-2-inc-all-safe.smt2		trees-2-inc-all-safe.smt2
trees-2-inc-all-unsafe.smt2		trees-2-inc-all-unsafe.smt2
trees-3-inc-some-safe.smt2		trees-3-inc-some-safe.smt2
trees-3-inc-some-unsafe.smt2		trees-3-inc-some-unsafe.smt2
trees-4-inc-some2-safe.smt2		trees-4-inc-some2-safe.smt2
trees-4-inc-some2-unsafe.smt2		trees-4-inc-some2-unsafe.smt2

Repository files navigation

Benchmarks from RustHorn for the TOPLAS 2021 paper. Generated from verification of small Rust programs.

Submitted to CHC-COMP-23 by Hari Govind V K

original repo. commit.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Repository files navigation

About

Releases

Packages

Languages

chc-comp/rust-horn

Folders and files

Latest commit

History

Repository files navigation

About

Resources

Stars

Watchers

Forks

Releases

Packages 0

Languages

Packages