Investigate Benchmarks from Hong & Ryu 2023 (ICSE '23)

[michael-schwarz]

In this recent work by Hong & Ryu https://arxiv.org/pdf/2301.10943.pdf, they used Goblint as part of the baseline toolchain they compared with.

p. 9 has a long table of benchmark programs. Those are interesting in two ways:

• Maybe we can use the benchmarks in our evaluations? They are concurrent pthread programs afaics.
• They report crashes for quite a few programs, might be worth looking into what's going on there.

They have a replication package here that probably also contains the benchmarks: https://zenodo.org/record/7573490

[vesalvojdani]

This is a very good suite!

• There are 46 programs with well-defined inclusion criteria that all use pthread.
• They have all the goblint-cil 1.8.2 merged files here: https://github.com/kaist-plrg/concrat/tree/master/bench
• Cello and pigz seem to use setjmp/longjmp.

[sim642]

These have now been merged into our suite and basic investigation has been done and documented. More thorough per-benchmark investigation is to be done separately for the PDLI paper.