Verifying temporal properties. Need problems.

[Yermat]

Bjorn Heimir Bjornsson wrote:
> 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

Hi,

I do not have any python program to check but I'm interested in 
publications you might already have writen or pointers to python related 
problem.
I'm working as engineer in a research team in formal methods area 
(http://www.loria.fr/equipes/model/).

Did you look at similar project with Java (like 
http://bandera.projects.cis.ksu.edu/) ? I think you will find similar 
problem, no ?

Did your prototype recognize use of the thread standard library (lock, 
etc) ?

If you look at mailman (http://www.list.org/), you can check security 
property like "a non-members cannot send messages to the list", etc.

Do you look at rather small or big project ?

Sorry if I ask more question than I answer... ;-)
The last one : When will you finish your Phd ?

Loïc