[TIP] Model checking Python code

[C. Titus Brown]

On Fri, Sep 04, 2009 at 06:45:57PM +0100, Mark Seaborn wrote:
-> I recently wrote up some notes on how to do model checking in Python
-> based on the technique used in eXplode:
-> http://lackingrhoticity.blogspot.com/2009/08/how-to-do-model-checking-of-python-code.html
-> 
-> (This is somewhat misnamed because it is not *model* checking -- it
-> involves testing real code, not a model of the code -- but I don't have
-> a better term for it yet.)
-> 
-> So far I have only used this technique on a small scale, to generate
-> test input, but I'd like to see if people here have ideas about how this
-> technique could be put to use in test frameworks.
-> 
-> Model checking has traditionally been used to explore systems with large
-> choice trees.  eXplode tests storage systems (Linux filesystems and
-> VCSes) for crash-resistance, and the choice tree of the test is
-> infinite.  It can take days to explore the choice tree by a useful
-> amount in order to discover bugs.  (However, once the path to a bug is
-> found it can be reproduced quickly.)

Hi, Mark,

I know of one person, Tao Xie, who is doing this with .NET code.

http://people.engr.ncsu.edu/txie/research.htm
http://sites.google.com/site/teachpex/Home

It's a bit hard to get more information about the project online -- I
saw a talk by him that was interesting.  We talked briefly about him
applying it to Python, too; he was intrigued to find out that people
actually used Python for big programming projects ;)

cheers,
--titus
-- 
C. Titus Brown, ctb at msu.edu