Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

View and Validate the Witness

• View Witness
• 
  Click on the button to verify this program using this witness, and inpect the validation results, e.g., explore the ARG or error path.

Input Given to this Service about the Witness (URL Query)

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/46e95d5b5de2d3ca622a1f55e109b60e55957bbfeb5d2c0b70ae3593799dc2fc.json

This witness was created for this program (cf. table above, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46).

Available Results for the Program from Witness Store SV-COMP '24

Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json

Available Results for the Program from Witness Store SV-COMP '23

Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json

Available Results for the Program from Witness Store SV-COMP '22

Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json

Available Results for the Program from Witness Store SV-COMP '21

Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json

Available Results for the Program from Witness Store SV-COMP '20

Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json

Available Results for the Program from Witness Store SV-COMP '19

Found 13 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json

Show Witness	Inspect	Validate	Specification	Result Type	Producer	Size (kB)	Time stamp	Input Witness
3dc1653	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn b8d6131600+	16	2018-12-07T10:52:13+01:00
385d0a2	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	10	2018-12-10T10:48:48+01:00	ab7a466
098adaa	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	15	2018-12-09T21:49:40+01:00	6a8f184
916c907	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	15	2018-12-09T21:38:33+01:00	56f1471
0eb42d8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	13	2018-12-08T08:27:15+01:00	3dc1653
068a40f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	10	2018-12-08T04:35:39+01:00	ab7a466
9c01cf8	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	8	2018-12-06T19:53:38+01:00	5fcf854
46e95d5	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	13	2018-12-06T09:47:55+01:00	575170b
99143eb	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	10	2018-12-06T09:18:40+01:00	9b6dd55
bcee55f	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	10	2018-12-06T09:00:05+01:00	9b6dd55
575170b	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	violation_witness	CPAchecker 1.7-svn 29852	16	2018-12-06T00:29:42+01:00
ae2104c	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	4	2018-12-09T20:54:17+01:00	314d0a4
d444160	Inspect		CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )	correctness_witness	CPAchecker 1.7-svn 29852	4	2018-12-09T20:41:30+01:00	e36ff1d

Available Results for the Program from Witness Store SV-COMP '18

Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json

Available Results for the Program from Witness Store SV-COMP '17

Found 0 witnesses for program sv-benchmarks/c/pthread/triangular_false-unreach-call.i, 8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8b3aa167dddace7806396759e5ce614de031a34926455878b96cabd1007abb46.json