{"action":"created","issue":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/270","repository_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks","labels_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/270/labels{/name}","comments_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/270/comments","events_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/270/events","html_url":"https://github.com/sosy-lab/sv-benchmarks/issues/270","id":192100864,"number":270,"title":"Category Organization for SV-COMP 2017","user":{"login":"dbeyer","id":2941008,"avatar_url":"https://avatars.githubusercontent.com/u/2941008?v=3","gravatar_id":"","url":"https://api.github.com/users/dbeyer","html_url":"https://github.com/dbeyer","followers_url":"https://api.github.com/users/dbeyer/followers","following_url":"https://api.github.com/users/dbeyer/following{/other_user}","gists_url":"https://api.github.com/users/dbeyer/gists{/gist_id}","starred_url":"https://api.github.com/users/dbeyer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dbeyer/subscriptions","organizations_url":"https://api.github.com/users/dbeyer/orgs","repos_url":"https://api.github.com/users/dbeyer/repos","events_url":"https://api.github.com/users/dbeyer/events{/privacy}","received_events_url":"https://api.github.com/users/dbeyer/received_events","type":"User","site_admin":false},"labels":[{"id":472370233,"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/labels/category%20definitions","name":"category definitions","color":"fbca04","default":false}],"state":"open","locked":false,"assignee":{"login":"tautschnig","id":1144736,"avatar_url":"https://avatars.githubusercontent.com/u/1144736?v=3","gravatar_id":"","url":"https://api.github.com/users/tautschnig","html_url":"https://github.com/tautschnig","followers_url":"https://api.github.com/users/tautschnig/followers","following_url":"https://api.github.com/users/tautschnig/following{/other_user}","gists_url":"https://api.github.com/users/tautschnig/gists{/gist_id}","starred_url":"https://api.github.com/users/tautschnig/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tautschnig/subscriptions","organizations_url":"https://api.github.com/users/tautschnig/orgs","repos_url":"https://api.github.com/users/tautschnig/repos","events_url":"https://api.github.com/users/tautschnig/events{/privacy}","received_events_url":"https://api.github.com/users/tautschnig/received_events","type":"User","site_admin":false},"assignees":[{"login":"tautschnig","id":1144736,"avatar_url":"https://avatars.githubusercontent.com/u/1144736?v=3","gravatar_id":"","url":"https://api.github.com/users/tautschnig","html_url":"https://github.com/tautschnig","followers_url":"https://api.github.com/users/tautschnig/followers","following_url":"https://api.github.com/users/tautschnig/following{/other_user}","gists_url":"https://api.github.com/users/tautschnig/gists{/gist_id}","starred_url":"https://api.github.com/users/tautschnig/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tautschnig/subscriptions","organizations_url":"https://api.github.com/users/tautschnig/orgs","repos_url":"https://api.github.com/users/tautschnig/repos","events_url":"https://api.github.com/users/tautschnig/events{/privacy}","received_events_url":"https://api.github.com/users/tautschnig/received_events","type":"User","site_admin":false},{"login":"dbeyer","id":2941008,"avatar_url":"https://avatars.githubusercontent.com/u/2941008?v=3","gravatar_id":"","url":"https://api.github.com/users/dbeyer","html_url":"https://github.com/dbeyer","followers_url":"https://api.github.com/users/dbeyer/followers","following_url":"https://api.github.com/users/dbeyer/following{/other_user}","gists_url":"https://api.github.com/users/dbeyer/gists{/gist_id}","starred_url":"https://api.github.com/users/dbeyer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dbeyer/subscriptions","organizations_url":"https://api.github.com/users/dbeyer/orgs","repos_url":"https://api.github.com/users/dbeyer/repos","events_url":"https://api.github.com/users/dbeyer/events{/privacy}","received_events_url":"https://api.github.com/users/dbeyer/received_events","type":"User","site_admin":false}],"milestone":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/milestones/1","html_url":"https://github.com/sosy-lab/sv-benchmarks/milestones/SV-COMP'17","labels_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/milestones/1/labels","id":2159339,"number":1,"title":"SV-COMP'17","description":"","creator":{"login":"PhilippWendler","id":2545335,"avatar_url":"https://avatars.githubusercontent.com/u/2545335?v=3","gravatar_id":"","url":"https://api.github.com/users/PhilippWendler","html_url":"https://github.com/PhilippWendler","followers_url":"https://api.github.com/users/PhilippWendler/followers","following_url":"https://api.github.com/users/PhilippWendler/following{/other_user}","gists_url":"https://api.github.com/users/PhilippWendler/gists{/gist_id}","starred_url":"https://api.github.com/users/PhilippWendler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/PhilippWendler/subscriptions","organizations_url":"https://api.github.com/users/PhilippWendler/orgs","repos_url":"https://api.github.com/users/PhilippWendler/repos","events_url":"https://api.github.com/users/PhilippWendler/events{/privacy}","received_events_url":"https://api.github.com/users/PhilippWendler/received_events","type":"User","site_admin":false},"open_issues":4,"closed_issues":2,"state":"open","created_at":"2016-11-27T16:30:27Z","updated_at":"2016-11-28T19:52:27Z","due_on":"2016-12-03T00:00:00Z","closed_at":null},"comments":6,"created_at":"2016-11-28T19:52:10Z","updated_at":"2016-11-29T08:41:10Z","closed_at":null,"body":"There are still open implicit benchmark submissions that we have to handle,\r\ni.e., stow into the category hierarchy.\r\nIn the community meeting, we discussed and agreed on:\r\n\r\n> Matthias Heizmann (Ultimate) proposes to check Termination in all categories.\r\n\r\nMichael Tautschnig and I had implemented this yesterday and today.\r\n\r\nThe \"all categories\" should be interepreted as \"as many categories as possible\".\r\nCompare with issue #268 by @PhilippWendler \r\n\r\n> Zvonimir Rakamaric (Smack) proposes to check Overflows in all categories.\r\n> Zvonimir Rakamaric (Smack) proposes to check MemorySafety in all categories.\r\n\r\nOverflows is pretty straight forward how to extend.\r\n\r\nFor MemorySafety, I wonder which categories we could add here.\r\nShall we stay with HeapMemSafety and ArrayMemSafety for now?\r\nBesides this, we have a few marked as _false-invalid-deref\r\nin the meanwhile that we could add.\r\n(The original files that were left over when fixing undefined behavior that\r\n was originally not intended.)\r\n\r\nHere a graphical visualization of what I have understood so far:\r\nhttps://sv-comp.sosy-lab.org/2017/categories.svg\r\n\r\nAfter some discussion (and before Friday), I need to have a proposal for a new structure ready\r\nto give to the jury to vote on.\r\nFrom Friday onwards (as agreed on the mailing list) we should not change\r\nthe pairs (program, property), in other words, all proposals and benchmark additions\r\nhave Friday as deadline."},"comment":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/comments/263509409","html_url":"https://github.com/sosy-lab/sv-benchmarks/issues/270#issuecomment-263509409","issue_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/270","id":263509409,"user":{"login":"PhilippWendler","id":2545335,"avatar_url":"https://avatars.githubusercontent.com/u/2545335?v=3","gravatar_id":"","url":"https://api.github.com/users/PhilippWendler","html_url":"https://github.com/PhilippWendler","followers_url":"https://api.github.com/users/PhilippWendler/followers","following_url":"https://api.github.com/users/PhilippWendler/following{/other_user}","gists_url":"https://api.github.com/users/PhilippWendler/gists{/gist_id}","starred_url":"https://api.github.com/users/PhilippWendler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/PhilippWendler/subscriptions","organizations_url":"https://api.github.com/users/PhilippWendler/orgs","repos_url":"https://api.github.com/users/PhilippWendler/repos","events_url":"https://api.github.com/users/PhilippWendler/events{/privacy}","received_events_url":"https://api.github.com/users/PhilippWendler/received_events","type":"User","site_admin":false},"created_at":"2016-11-29T08:41:10Z","updated_at":"2016-11-29T08:41:10Z","body":"`Safety` seems to be a too general name. It looks like its is a super-category of `Thread-Safety` and `Memory-Safety`, and actually the issues in `Definedness` are also safety properties.\r\n\r\nI am not sure I like `Thread-Safety`, to me this name looks more like an implicit property of finding races etc., not like checking a given specification for a concurrent program.\r\n\r\nI think we should keep `Memory-Safety` consisting of the three sub-properties. If we change this, this would be a major change to the way how properties are used in SV-Comp and might even require changes to the verifiers, because so far these three properties were only used together. Also I think that this category matches existing tools well. From a verifier perspective, the three memory-safety properties have more in common than e.g. `valid-free` with `no-overflow`."}}
{"actor":{"display_login":"PhilippWendler"}}