TESLA assertions can be predicated on argument and return values of functions. In order to properly model check even simple examples, we need to augment the event structure with information about what we know about program values at the time an event is reached.
TESLA assertions can be predicated on argument and return values of functions. In order to properly model check even simple examples, we need to augment the event structure with information about what we know about program values at the time an event is reached.