An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
Some of these are a bit ad-hoc in that we call try_wait and it doesn't say the process has terminated, but z3 has returned an empty response. It's possible that z3 is in the middle of terminating in these cases, because calling wait seems to work.
Some of these are a bit ad-hoc in that we call try_wait and it doesn't say the process has terminated, but z3 has returned an empty response. It's possible that z3 is in the middle of terminating in these cases, because calling wait seems to work.