sosy-lab/sv-benchmarks

Category Structure for SV-COMP 2020

dbeyer opened this issue · 3 comments

dbeyer commented

How to best integrate new benchmark sets:

  • #798 OpenBSD: Own sub-category or part of existing sub-category?
  • #803 VerifyThis: Recursive examples have heap manipulation, move there?
  • #817 AWS C Common
  • #808 Programs with nonlinear properties
  • Split DeviceDrivers into small (<10 kLOC), medium (<100 kLOC), large (>=100 kLOC)
    Add ldv-challenges to the category of large driver tasks.
  • Juliet
dbeyer commented

Status on 2019-11-16:

  • #798 OpenBSD: Own sub-category or part of existing sub-category?
    • Created own sub-category of SoftwareSystems: SoftwareSystems-OpenBSD-MemSafety
  • #803 VerifyThis: Recursive examples have heap manipulation, move there?
    • Merged into ReachSafety-Loops and ReachSafety-Recursive
  • #817 AWS C Common
    • Created own sub-category of SoftwareSystems: SoftwareSystems-AWS-C-Common-ReachSafety
  • #808 Programs with nonlinear properties
    • Merged into ReachSafety-Loops
  • Split DeviceDrivers into small (<10 kLOC), medium (<100 kLOC), large (>=100 kLOC)
    Add ldv-challenges to the category of large driver tasks.
    • Done in pull request #926, but only for large (>=100 kLOC) for now.
  • Juliet
    • In progress.
MartinSpiessl commented

In the community meeting we discussed that for SV-COMP 2021 we should try to at least have a subset of the Juliet tasks.
So I would close this Issue and create a new one for the category structure of SV-COMP 2021

All that was left in this issue was the Juliet tasks if I see this correctly.

MartinSpiessl commented

I created a new issue for the category structure of SV-COMP 2021, cf. #1127