Pluripotency is the unique characteristic of embryonic stem (ES) cells, which demonstrate the capacity to generate all somatic cell lineages. But how ES cells decide to transition to a given adult cell type remains unknown. In this project, we combine formal verification, model-checking and model synthesis into a new tool for uncovering the transcriptional program of pluripotency: a reasoning engine for interaction networks.
The tool can also be run with examples pre-loaded. For further information on these examples, please refer to the tutorial.
Simple four-component example
Basic stem cell pluripotency example, constrained against 15 experimental observations
Stem cell pluripotency example, constrained against 23 experimental observations
Identifying the minimal transcriptional network governing pluripotency. In this example, set the interaction limit to 17.
The examples that are referred to throughout the tutorial are available here. These can be loaded and run as instructed.
- Sara-Jane Dunn, Graziano Martello, Boyan Yordanov, Stephen Emmott, and Austin Smith, Defining an essential transcriptional factor program for naïve pluripotency, in Science, vol. 344, no. 6188, pp. 1156 - 1160, 6 June 2014
Windows bug-testing software cracks stem cell programs - New Scientist
Minimal toolkit for stem cell self-renewal - The Scientist
Theorem prover sheds new light on stem cell behaviour - Inside Microsoft Research