Verifying temporal properties. Need problems.

[Bjorn Heimir Bjornsson]

Hello all

As part of a thesis, I am model checking Python programs (a limited
subset anyway).

I have a very rough prototype that can deal with temporal properties
(LTL), that is statically prove properties of the kind: "if A happens,
then B should follow" or "if A happens, then B must not follow unless
C happens first". A,B,C here being function calls (system or other
library). The idea is that this might complement testing or manual
auditing during development.

So the solution now requires a problem.
Basically I'm trying to find interesting areas where a programmer is
supposed to call specific functions in a particular order, but where
coding errors might prevent this.
I would be most happy with distinctively Python-related problems, like
some tricky-to-use system calls or something from Zope or
security-related issues, etc.

So if any of you have ideas (specific function calls) where this kind
of tool would be useful, I would welcome feedback.
If replying privately, use bjornhb2_hotmail.com (more or less).

Thanks a lot :)
Bjorn