Stochastic Models:
Scalable Model Checking. 
Home  Members  Meetings  Tasks  Publications  Bibliography 
Large stochastic systems arise naturally in many different contexts: from networks to system biology.
A model for Hela cells death and a model of stress response in yeast.

It consists in describing formally a system in the form of a mathematical model, specifying the properties it has to fulfill in a formal logic, and providing algorithms to decide whether the model satisfies the property.
Model checking started with Boolean systems and properties (sequential finite state models...).
Work extremely well for verifying (large, sequential) programs with Boolean predicates (x\leq a).
