{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:56:17Z","timestamp":1762865777395},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642182747"},{"type":"electronic","value":"9783642182754"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_11","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T05:06:38Z","timestamp":1295240798000},"page":"134-149","source":"Crossref","is-referenced-by-count":25,"title":["Proving Stabilization of Biological Systems"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Jasmin","family":"Fisher","sequence":"additional","affiliation":[]},{"given":"Elzbieta","family":"Krepska","sequence":"additional","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Fisher, J., Henzinger, T.A.: Executable biology. In: Proc. WSC, pp. 1675\u20131682 (2006)","DOI":"10.1109\/WSC.2006.322942"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-05089-3_2","volume-title":"FM 2009: Formal Methods","author":"N. Bonzanni","year":"2009","unstructured":"Bonzanni, N., Feenstra, A.K., Fokkink, W., Krepska, E.: What can formal methods bring to systems biology? In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 16\u201322. Springer, Heidelberg (2009)"},{"key":"11_CR3","series-title":"LNBI","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-03845-7_2","volume-title":"Computational Methods in Systems Biology","author":"J. Heath","year":"2009","unstructured":"Heath, J.: The equivalence between biology and computation. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS (LNBI), vol.\u00a05688, pp. 18\u201325. Springer, Heidelberg (2009)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Fisher, J., et al.: Predictive modeling of signaling crosstalk during C. elegans Vulval Development. PLoS CB 3(5), e92 (2007)","DOI":"10.1371\/journal.pcbi.0030092"},{"key":"11_CR5","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11885191_3","volume-title":"Computational Methods in Systems Biology","author":"J. Heath","year":"2006","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, G., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol.\u00a04210, pp. 32\u201347. Springer, Heidelberg (2006)"},{"key":"11_CR6","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-88562-7_18","volume-title":"Computational Methods in Systems Biology","author":"E. Clarke","year":"2008","unstructured":"Clarke, E., Faeder, J., Langmead, C., Harris, L., Jha, S., Legay, A.: Statistical model checking in BioLab: Applications to the automated analysis of T-Cell receptor signaling pathway. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 231\u2013250. Springer, Heidelberg (2008)"},{"issue":"1","key":"11_CR7","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2004.03.063","volume":"325","author":"N. Chabrier-Rivier","year":"2004","unstructured":"Chabrier-Rivier, N., Chiaverini, M., Danos, V., Fages, F., Sch\u00e4chter, V.: Modeling and querying biomolecular interaction networks. Theo. Comp. Sci.\u00a0325(1), 25\u201344 (2004)","journal-title":"Theo. Comp. Sci."},{"key":"11_CR8","doi-asserted-by":"publisher","DOI":"10.1515\/9783110849974","volume-title":"The stable state of organisms in thermodynamic bases of biological processes: Physiological Reactions and Adaptations","author":"A.I. Zotin","year":"1990","unstructured":"Zotin, A.I.: The stable state of organisms in thermodynamic bases of biological processes: Physiological Reactions and Adaptations. De Gruyter, Berlin (1990)"},{"key":"11_CR9","unstructured":"Jones, C.: Specification and design of (parallel) programs. In: IFIP Congr. 1983, pp. 321\u2013332 (1983)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, pp. 123\u2013144 (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"issue":"1","key":"11_CR11","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. TOPLAS\u00a015(1), 73\u2013132 (1993)","journal-title":"TOPLAS"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Schaub, M., et al.: Qualitative networks: A symbolic approach to analyze biological signaling networks. BMC Systems Biology\u00a01, 4 (2007)","DOI":"10.1186\/1752-0509-1-4"},{"issue":"2","key":"11_CR13","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF02460618","volume":"55","author":"R. Thomas","year":"1995","unstructured":"Thomas, R., Thieffry, D., Kaufman, M.: Dynamical behaviour of biological regulatory networks\u2014I. Biological role of feedback loops and practical use of the concept of the loop-characteristic state. Bullet. of Math.\u00a0Bio.\u00a055(2), 247\u2013276 (1995)","journal-title":"Bullet. of Math.\u00a0Bio."},{"key":"11_CR14","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-75140-3_16","volume-title":"Computational Methods in Systems Biology","author":"A. Naldi","year":"2007","unstructured":"Naldi, A., Thieffry, D., Chaouiya, C.: Decision diagrams for the representation and analysis of logical models of genetic networks. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol.\u00a04695, pp. 233\u2013247. Springer, Heidelberg (2007)"},{"issue":"9","key":"11_CR15","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.159839","volume":"18","author":"N. Halbwachs","year":"1992","unstructured":"Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying critical systems by means of the synchronous data-flow programming language LUSTRE. IEEE Transactions on Software Engineering\u00a018(9), 785\u2013793 (1992)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR17","unstructured":"Beyer, A., Fisher, J.: Unpublished results (2009)"},{"key":"11_CR18","series-title":"LNBI","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-11712-1_4","volume-title":"Transactions on Computational Systems Biology XII","author":"A. Beyer","year":"2010","unstructured":"Beyer, A., et al.: Mechanistic insights into metabolic disturbance during type-2 diabetes and obesity using qualitative networks. In: Priami, C., Breitling, R., Gilbert, D., Heiner, M., Uhrmacher, A.M. (eds.) Transactions on Computational Systems Biology XII. LNCS (LNBI), vol.\u00a05945, pp. 146\u2013162. Springer, Heidelberg (2010)"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1016\/S0022-5193(03)00201-7","volume":"224","author":"L. Sanchez","year":"2003","unstructured":"Sanchez, L., Thieffry, D.: Segmenting the fly embryo: a logical analysis fo the pair-rule cross-regulatory module. Journal of Theoretical Biology\u00a0224, 517\u2013537 (2003)","journal-title":"Journal of Theoretical Biology"},{"key":"11_CR20","unstructured":"Ropers, D., Baldazzi, V., de Jong, H.: Model reduction using piecewise-linear approximations preserves dynamic properties of the carbon starvation response in E. coli. IEEE\/ACM Trans. on Comp. Bio. and Bioinf. 99 (2009) (preprint)"},{"issue":"1","key":"11_CR21","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1049\/sb:20045019","volume":"1","author":"R. Ghosh","year":"2004","unstructured":"Ghosh, R., Tomlin, C.: Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: Delta-Notch protein signalling. IEE Systems Biology\u00a01(1), 170\u2013183 (2004)","journal-title":"IEE Systems Biology"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1007\/978-3-540-71493-4_76","volume-title":"Hybrid Systems: Computation and Control","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 750\u2013753. Springer, Heidelberg (2007)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-00602-9_20","volume-title":"Hybrid Systems: Computation and Control","author":"J. Oehlerking","year":"2009","unstructured":"Oehlerking, J., Theel, O.: Decompositional construction of Lyapunov functions for hybrid systems. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol.\u00a05469, pp. 276\u2013290. Springer, Heidelberg (2009)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: Proc. POPL, pp. 265\u2013276 (2007)","DOI":"10.1145\/1190216.1190257"},{"issue":"2","key":"11_CR25","first-page":"213","volume":"14","author":"J.S. Moore","year":"1999","unstructured":"Moore, J.S.: A mechanically checked proof of a multiprocessor result via a uniprocessor view. FMSD\u00a014(2), 213\u2013228 (1999)","journal-title":"FMSD"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"K. McMillan","year":"1999","unstructured":"McMillan, K.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 342\u2013345. Springer, Heidelberg (1999)"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Practical Methods for Proving Program Termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"issue":"9","key":"11_CR29","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1016\/S0960-9822(00)00451-6","volume":"4, 10","author":"S. Lowell","year":"2000","unstructured":"Lowell, S., et al.: Stimulation of human epidermal differentiation by delta-notch signalling at the boundaries of stem-cell clusters. Curr. Biol.\u00a04, 10(9), 491\u2013500 (2000)","journal-title":"Curr. Biol."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. In: Proc. FMSD, vol.\u00a019(1), pp. 7\u201334 (2001)","DOI":"10.1023\/A:1011276507260"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Proc. FMICS. ENTCS, vol.\u00a066(2), pp. 160\u2013177 (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Symbolic model checking (PhD thesis). Kluwer (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura De","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 359. Springer, Heidelberg (2002)"},{"key":"11_CR35","unstructured":"Holzmann, G.: The SPIN model checker: Primer and ref. manual. Wesley (2003)"},{"key":"11_CR36","unstructured":"Cook, B., Fisher, J., Krepska, E., Piterman, N.: Proving stabilization of biological systems: Appendix. Technical Teport IR-CS-63"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18275-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T22:39:30Z","timestamp":1559947170000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}