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/floats-cdfpl/sine_2_false-unreach-call_true-termination.i
programSHA fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
witnessName results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-reachsafety.sine_2_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 978f1fd18d4881e1e11b7a2c859bed48bcd67c7ab71f21979a9af98ed37e405e

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/978f1fd18d4881e1e11b7a2c859bed48bcd67c7ab71f21979a9af98ed37e405e.json

Key Value
architecture 32bit
creationtime 2018-12-07T22:18:36.425133
producer ESBMC 6.0.0 kind
programfile ../../sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i
programhash 79593329bc8f7511983805b3e0e5d4c7fc3a0674
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/978f1fd18d4881e1e11b7a2c859bed48bcd67c7ab71f21979a9af98ed37e405e.graphml
witness-sha256 978f1fd18d4881e1e11b7a2c859bed48bcd67c7ab71f21979a9af98ed37e405e
witness-size 4225
witness-type violation_witness

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

Trying to find witnesses for program (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.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 (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.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 (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.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 (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.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 (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 16 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 54c4006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-04T00:06 CET (comp)
Download 26c3163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:49:08+01:00 Download ec1edbd
Download 207d34c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:52:41+01:00 Download bba5b7d
Download 8e049f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T19:34:05+01:00 Download 0bd466b
Download 36bf949 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:01:20+01:00 Download f671d1f
Download f671d1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 5 2019-11-29T15:36:39+01:00
Download bba5b7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 3 2019-12-07T12:50:38+01:00
Download ec1edbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T12:49:34+01:00
Download 30ba622 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness BRICK 4 2019-12-07T21:40:49Z
Download 1116308 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T21:09:01+01:00 Download 632bf7a
Download d6a3931 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:55:17+01:00 Download 454bdee
Download a07d5d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:44:37+01:00 Download 579afb0
Download 7b8f6dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:51:12+01:00 Download 30ba622
Download 88b0d3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T20:20:33+01:00 Download 544830f
Download 4a27afa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:58:43+01:00 Download 54c4006
Download 390b0a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:35 CET (comp)

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

Trying to find witnesses for program (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f8b8678 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-07T09:15 CET (sv-comp)
Download f2bb48e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 4 2018-12-10T17:07:29+01:00
Download d2bc549 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T14:17:46+01:00
Download 8377a33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:35:49+01:00 Download f2bb48e
Download 17b2dc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:54+01:00 Download 85e6c4c
Download 5315da4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:38:51+01:00 Download f31302d
Download 7bde0f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:22:19+01:00 Download 5b7ad02
Download df259dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T09:05:23+01:00 Download d2bc549
Download b73b2e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T18:48:13+01:00 Download 18d8ddb
Download 8087a8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:44:21+01:00 Download f8b8678
Download 8619eb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:54+01:00 Download 8f06ffb
Download 13ffb7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:41:05+01:00 Download 8c7d970
Download 9b00ef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:05:59+01:00 Download 0c56f86
Download 8f06ffb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T01:02:54+01:00
Download e3cc54e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:59:06+01:00 Download 978f1fd
Download abdee24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T10:16:18+01:00 Download 4a3b343
Download 14155a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:18:14+01:00 Download 259813e
Download 17b2a34 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T08:58 CET (sv-comp)

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

Trying to find witnesses for program (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 064d083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:13 CET (sv-comp)
Download f7a90dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-03T03:02Z
Download 7a843af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T21:13:13.275919
Download fc9f8dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T14:26:32.824776
Download 7791cb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T20:25 CET (sv-comp)
Download 6a6038c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T17:12 CET (sv-comp)
Download 0e698ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-03T00:51:06+01:00
Download 6cfac77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T13:14:33+01:00
Download 3ff77e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-12-01T02:00:38+01:00
Download 0e3abba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T12:52:09+01:00
Download f431dc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T04:47:05+01:00
Download 0b81b59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-12-01T03:34 CET (sv-comp)
Download a669624 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T14:39Z
Download 158bacf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-12-01T03:52 CET (sv-comp)
Download 621dddd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:29:53.586475
Download 6879897 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:14:41.857437
Download 3808bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T13:13 CET (sv-comp)
Download 6d33be7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T16:12 CET (sv-comp)

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

Trying to find witnesses for program (fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920, sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/floats-cdfpl/sine_2_false-unreach-call_true-termination.i, fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/fc61f411650ed0513604e7c2fc4f7236bd85ec5cb7bf12d7f380d06fd86ae920.json

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