Advices wanted on modeling finite executions

Stream: Program verification

[Ching-Tsun Chou]

I asked the following question in the channel general. In retrospect, perhaps I should have asked it in this channel instead. I would very much like to get some feedbacks. Please post your comments at my original post below. Thanks in advance!

#general > Advices wanted on modeling finite executions