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

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

Key Value
programName sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c
programSHA 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
witnessName results-verified/uautomizer.2017-12-03_1212.logfiles/sv-comp18.Problem14_label43_false-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 1370466dc9811145376fa83b49c035a3e674225719f7eb75d15db107a04fe63d

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/1370466dc9811145376fa83b49c035a3e674225719f7eb75d15db107a04fe63d.json

Key Value
architecture 32bit
creationtime 2017-12-03T11:16Z
producer Automizer
program-sha256 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
programfile /tmp/vcloud-vcloud-master/worker/working_dir_bf3442bb-862a-47b6-90a3-7918fe65b061/sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c
programhash aaebc66109211c5340229485760e37fee1256d9e
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/1370466dc9811145376fa83b49c035a3e674225719f7eb75d15db107a04fe63d.graphml
witness-sha256 1370466dc9811145376fa83b49c035a3e674225719f7eb75d15db107a04fe63d
witness-size 147006
witness-type violation_witness

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download dff981b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 4 2019-12-01 03:34:53
Download b9f4456 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 385 2019-12-03T23:37 CET (comp)
Download 11f186d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1235 2019-12-11T21:09:48+01:00 Download dff981b
Download 678f7c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1236 2019-12-11T20:44:41+01:00 Download 357096b
Download 699dee7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1536 2019-12-04T02:58:15+01:00 Download b9f4456
Download 8ffa03e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1235 2019-12-03T08:10:01+01:00 Download 2e37c96
Download 2e37c96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 1235 2019-11-29T15:57:41+01:00
Download c3b9c62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 301 2019-12-11T20:55:17+01:00 Download 6ed86dc
Download 306f772 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 301 2019-12-07T21:18:09+01:00 Download b886a3c
Download 0dd5d70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 301 2019-12-05T20:22:20+01:00 Download e34ece7
Download 5558397 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 01:07:14

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7a39642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T08:39 CET (sv-comp)
Download a10a833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 451 2018-12-07T15:47 CET (sv-comp)
Download 40afcf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 1240 2018-12-08T00:36:59+01:00
Download 6db6ce1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1236 2018-12-09T17:49:14+01:00 Download c8a0b17
Download e6994fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1235 2018-12-08T07:52:28+01:00 Download 40afcf4
Download 7dedc6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1536 2018-12-07T17:45:12+01:00 Download a10a833
Download 253c2f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1235 2018-12-06T09:48:22+01:00 Download 3e84e3f
Download 8e717b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1846 2018-12-06T09:15:53+01:00 Download f752e7b
Download 3e84e3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1235 2018-12-05T17:28:58+01:00
Download 4577f9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-10T20:37:17+01:00 Download 361f939
Download 3ee69b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-09T20:53:57+01:00 Download e507cee
Download c145810 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-09T20:38:35+01:00 Download cb15566
Download ee0f38b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-08T23:45:05+01:00 Download 7a39642
Download 63cb6f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-08T05:01:59+01:00 Download 4a5b11b
Download 8a14749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-06T10:19:25+01:00 Download 11f2d43
Download e2ea11a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-06T09:44:05+01:00 Download 1bd45cb

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2c892a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 813 Sat Dec 2 22:47:44 2017
Download a1d4733 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:14 CET (sv-comp)
Download de6da5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 8 2017-12-01T12:22:09.763904
Download b15225e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 8 2017-12-01T17:15:48.140548
Download c81bd86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 22 2017-12-01T15:28 CET (sv-comp)
Download 1b0d685 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 662 2017-12-01T00:01:29+01:00
Download 37825a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 884 2017-11-30T15:03:53+01:00
Download 17d4570 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 659 2017-12-01T03:03:32+01:00
Download 5aebb4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 505 2017-12-01T01:12 CET (sv-comp)
Download f9b20df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 949 2017-12-02T18:35Z
Download 6875c35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 510 2017-12-01T00:17 CET (sv-comp)
Download 1370466 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 147 2017-12-03T11:16Z
Download 9d0cba0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 577 2017-12-01T13:48 CET (sv-comp)

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

Trying to find witnesses for program (3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb, sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c, 3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3b18250e4e8ae1ec6302837c473ab1c99a17fa8cb4d02c96a4cf4c8b22b10cfb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness