sv-witnesses icon indicating copy to clipboard operation
sv-witnesses copied to clipboard

Published 20 hours ago • verified publisher icon sosy-lab

Specification fix: ensure that the initial thread can be referenced

Open tautschnig opened this issue 3 years ago • 1 comments

With the previous specification, the initially active thread (as created by starting a program) could not be referenced in transitions without violating the specification (only threads specified in createThread could be referenced).

~Marked as Draft as #29 should be merged first and~ we shouldn't change the spec while SV-COMP'21 is about to kick off, so let's not merge until after SV-COMP'21 has been fully executed.

tautschnig avatar Dec 01 '20 20:12 tautschnig