Name
Abstract | ||
|---|---|---|
We describe the formal verification of two theorems of theoretical biology. These theorems concern genetic regulatory networks: they give, in a discrete modeling framework, relations between the topology and the dynamics of these biological networks.In the considered discrete modeling framework, the dynamics is described by a transition graph, where vertices are vectors indicating the expression level of each gene, and where edges represent the evolution of these expression levels.The topology is also described by a graph, called interaction graph, where vertices are genes and where edges correspond to influences between genes. The two results we formalize show that circuits of some kind must be present in the interaction graph if some behaviors are possible in the transition graph. This work was performed with the ssreflect extension of the Coq system. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/SYNASC.2009.44 | SYNASC |
Keywords | Field | DocType |
formal verification,genetics,graph theory,theorem proving,Coq system,biological networks,discrete modeling framework,formal theorem proving,formal verification,genetic regulatory networks,interaction graph,ssreflect extension,theoretical biology,transition graph,coq system,formal proof,gene regulatory network | Graph theory,Discrete mathematics,Computer science,Biological network,Graph labeling,Quartic graph,Directed graph,Theoretical computer science,Null graph,Voltage graph,Complement graph | Conference |
ISSN | Citations | PageRank |
2470-8801 | 0 | 0.34 |
References | Authors | |
1 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maxime Dénès | 1 | 64 | 4.91 |
| Binjamin Lesage | 2 | 0 | 0.34 |
| Yves Bertot | 3 | 442 | 40.82 |
| Adrien Richard | 4 | 119 | 16.51 |