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/Problem02_label10_true-unreach-call_false-termination.c
programSHA 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-termination.Problem02_label10_true-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 002cdb8411c79d909cd9e4536a4deca3489f6c86498e4dadf73845a816f4b1fc

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/002cdb8411c79d909cd9e4536a4deca3489f6c86498e4dadf73845a816f4b1fc.json

Key Value
architecture 32bit
creationtime 2018-12-06T20:08:54+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001
programfile ../../sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c
programhash 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/002cdb8411c79d909cd9e4536a4deca3489f6c86498e4dadf73845a816f4b1fc.graphml
witness-sha256 002cdb8411c79d909cd9e4536a4deca3489f6c86498e4dadf73845a816f4b1fc
witness-size 359160
witness-type violation_witness

This witness was created for this program (cf. table above, 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001).

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

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

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c, 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001.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 (3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001, sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c, 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001.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 (3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001, sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c, 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001.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 (3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001, sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c, 3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001.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 (3afa693bc56b77c412b408a7e81af2a502911e5c5b18ef7e4be8989a8067b001, sv-benchmarks/c/eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c).

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 096c796 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:22:49+01:00 Download 43f8582
Download 741aac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:08:46+01:00 Download 7868c2f
Download 7c0d97e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-11T20:02:55+01:00 Download 562f649
Download e7a5f1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-08T01:00:01+01:00 Download b0063b9
Download 4013c83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T23:32:16+01:00 Download 45fc995
Download 9491abc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-07T19:44:32+01:00 Download 1e12813
Download 8c31348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-12-05T19:03:01+01:00 Download 0d82659
Download 5b51951 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 280 2019-11-30T17:17:02+01:00 Download ad604be
Download ad604be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 280 2019-11-30T07:43:34+01:00
Download 7868c2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 280 2019-11-30T20:44:01+01:00
Download a3b1795 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2019-12-01 12:05:21
Download 8fb306e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 359 2019-11-30T13:31:38+01:00
Download 5f7ea94 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 359 2019-12-01T00:49:03+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c1fcd6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:48:56
Download 5fa9d35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 280 2018-12-06T20:16:43+01:00
Download 57ff1ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-10T19:39:48+01:00 Download 477f256
Download a4593f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:25:11+01:00 Download a8bb1dc
Download 9dcc675 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T20:00:53+01:00 Download 9f0b8be
Download 8de0a56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-09T19:55:18+01:00 Download 8cabf77
Download c62c729 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T21:46:17+01:00 Download c1fcd6f
Download 6689d50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T06:20:55+01:00 Download 5fa9d35
Download da1fa9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-08T03:14:00+01:00 Download 6fd8d23
Download 50ebcd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:28:29+01:00 Download e6a5639
Download 05410ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T09:08:50+01:00 Download 6e2f92a
Download bb3bad8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-06T07:37:19+01:00 Download 84e9cab
Download 6e2f92a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 280 2018-12-05T09:45:35+01:00
Download 002cdb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 359 2018-12-06T20:08:54+01:00
Download de3767e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-08T08:58:51+01:00
Download 2530b13 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 356 2018-12-06T09:48:22+01:00
Download 7444a24 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 359 2018-12-05T22:34:01+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fe05cf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 161 2017-12-03T04:55Z
Download 6d1560f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 179 2017-12-02T14:56Z
Download 4d19817 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.12-svcomp17 4 2017-11-02T13:16:17+05:30
Download 7cacfaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T06:57:48+01:00 3dafc4d
Download b39f486 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T04:08:42+01:00 e6891d7
Download b0f8605 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T02:53:55+01:00 a061d0a
Download 820671f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-03T00:36:02+01:00 5dfb4bb
Download 3873a0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-02T15:29:48+01:00 82fbefd
Download a6ad7f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T06:37:59+01:00 2deea49
Download dcf3430 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:59:42+01:00 15d1b17
Download e3454c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T05:06:35+01:00 83aa901
Download 795f8c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-12-01T04:27:29+01:00 f9a1be5
Download cc6b943 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 280 2017-11-30T23:01:10+01:00
Download 687f417 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 337 2017-11-30T16:09:20+01:00
Download 91c9e23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 280 2017-11-30T20:11:22+01:00
Download 8a56b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 469 2017-12-01T20:10:21+01:00
Download 844d1a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 161 2017-12-02T10:23Z
Download 3e93e35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 811 2017-11-30T14:51 CET (sv-comp)
Download 6976830 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 334 2017-12-01T13:10:21+01:00
Download 3aeeead Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 15 2017-12-03T11:18Z
Download 19dc82b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 26 2017-12-01T15:05 CET (sv-comp)

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

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

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

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