Verifying temporal properties. Need problems.

[Yermat]

Bjorn Heimir Bjornsson a écrit :

> Hello Loic
> I'm working with control flow only, generating pushdown systems from the
> AST that are then checked with the model checker Moped (using LTL
> properties).
> A similar approach was taken for JavaCard
> (http://www.sics.se/fdt/vericode/jcave.html). 
> I chose Python for fun, but at the moment support just a limited subset.
> I'm unsure how far I will/can go. E.g. some dynamic stuff can't be analysed 
> statically. I also just ignore all data flow, which simplifies everything but 
> means I will not recognise all control flow correctly. 
> I checked some small non-python-specific problems, but experience of others 
> suggest that the aproach scales quite well. 
> This is an MSc thesis, I haven't published anything else. 
> Bjorn

Hi,
Ok I see.
Instead of searching the workflow yourself you might look at PyPY. There 
is a class (see translator.py) that construct such a flow. I have also 
construct a simple data flow to check if a variable used was previously 
defined.

On monday, I will show you a kind of workflow I'm creating in case mine 
is more complete than yours...

Anyway, you're right that with dinamic stuff, analysis is difficult. But 
with research like StarKiller (Type Inference) it should become more and 
more easier...

I will wait for your publication ;-)

Loïc