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/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c
programSHA 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
witnessName results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c.files/witness.graphml
witnessSHA a13a66fa181be84dfb130693f9a4a0ea0fb7dcde06d734941b8cfcb44a68757d

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2017-12-03T04:33 CET (sv-comp)
producer Symbiotic
program-sha256 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
programfile /tmp/vcloud-vcloud-master/worker/working_dir_685e095c-f790-4c02-97fe-117490e2eaac/sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c
programhash 8258a077de60ec345ee6a34df387bac654951e25
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/a13a66fa181be84dfb130693f9a4a0ea0fb7dcde06d734941b8cfcb44a68757d.graphml
witness-sha256 a13a66fa181be84dfb130693f9a4a0ea0fb7dcde06d734941b8cfcb44a68757d
witness-size 1280
witness-type violation_witness

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

Trying to find witnesses for program (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.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 (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.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 (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.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 (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.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 (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.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 '19

Trying to find witnesses for program (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.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 '18

Trying to find witnesses for program (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 20 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f1b93ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 4 2017-12-03T07:44Z
Download a13a66f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2017-12-03T04:33 CET (sv-comp)
Download 78de2df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 2 2017-12-02T01:12 CET (sv-comp)
Download a673f9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 4 2017-12-03T10:19Z
Download 6e3853d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T17:56:19.205545
Download 91a0d80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T06:02:03.144366
Download 1d339e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 3.1 4 2017-12-01T13:18 CET (sv-comp)
Download 46e3ff4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:59+01:00 043715d
Download 92e0849 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:10+01:00 d056a06
Download a883b4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T08:58:56+01:00 5ce205b
Download c9a07de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T05:18:09+01:00 ad004db
Download 9ea25d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:07:01+01:00 afc3229
Download d0a11d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:12:57+01:00 32e1275
Download 5b75fcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T12:31:38+01:00 4d15290
Download 34937e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T12:02:23+01:00 468d665
Download 1260638 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:41:32+01:00
Download 2eb3b98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:19:39+01:00 c4b1443
Download 4273b8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 3 2017-12-01T11:59 CET (sv-comp)
Download 990c60b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 4 2017-12-03T10:23Z
Download 771755e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 3 2017-12-01T10:21 CET (sv-comp)

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

Trying to find witnesses for program (59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef, sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c, 59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/59c531b839c87e8106f69c1a3266ed83442ab150588184528dd01502e48cabef.json

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