Verifying temporal properties. Need problems.

[Bjorn Heimir Bjornsson]

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