[{"date_created":"2018-12-11T11:48:07Z","page":"543 - 544","publication":"Acta Informatica","publication_status":"published","doi":"10.1007/s00236-017-0299-0","language":[{"iso":"eng"}],"department":[{"_id":"KrCh"}],"date_published":"2017-09-01T00:00:00Z","type":"journal_article","oa_version":"None","scopus_import":1,"publist_id":"6961","volume":54,"intvolume":"        54","quality_controlled":"1","citation":{"short":"K. Chatterjee, R. Ehlers, Acta Informatica 54 (2017) 543–544.","ama":"Chatterjee K, Ehlers R. Special issue: Synthesis and SYNT 2014. <i>Acta Informatica</i>. 2017;54(6):543-544. doi:<a href=\"https://doi.org/10.1007/s00236-017-0299-0\">10.1007/s00236-017-0299-0</a>","ieee":"K. Chatterjee and R. Ehlers, “Special issue: Synthesis and SYNT 2014,” <i>Acta Informatica</i>, vol. 54, no. 6. Springer, pp. 543–544, 2017.","chicago":"Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and SYNT 2014.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-017-0299-0\">https://doi.org/10.1007/s00236-017-0299-0</a>.","apa":"Chatterjee, K., &#38; Ehlers, R. (2017). Special issue: Synthesis and SYNT 2014. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-017-0299-0\">https://doi.org/10.1007/s00236-017-0299-0</a>","mla":"Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and SYNT 2014.” <i>Acta Informatica</i>, vol. 54, no. 6, Springer, 2017, pp. 543–44, doi:<a href=\"https://doi.org/10.1007/s00236-017-0299-0\">10.1007/s00236-017-0299-0</a>.","ista":"Chatterjee K, Ehlers R. 2017. Special issue: Synthesis and SYNT 2014. Acta Informatica. 54(6), 543–544."},"day":"01","year":"2017","date_updated":"2021-01-12T08:12:18Z","issue":"6","abstract":[{"lang":"eng","text":"The ubiquity of computation in modern machines and devices imposes a need to assert the correctness of their behavior. Especially in the case of safety-critical systems, their designers need to take measures that enforce their safe operation. Formal methods has emerged as a research field that addresses this challenge: by rigorously proving that all system executions adhere to their specifications, the correctness of an implementation under concern can be assured. To achieve this goal, a plethora of techniques are nowadays available, all of which are optimized for different system types and application domains."}],"_id":"719","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Ehlers, Rüdiger","last_name":"Ehlers","first_name":"Rüdiger"}],"title":"Special issue: Synthesis and SYNT 2014","publication_identifier":{"issn":["00015903"]},"status":"public","publisher":"Springer","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","month":"09"},{"external_id":{"isi":["000414343200003"]},"quality_controlled":"1","volume":54,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1835"}]},"publist_id":"5898","article_processing_charge":"No","pubrep_id":"649","type":"journal_article","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"has_accepted_license":"1","date_created":"2018-12-11T11:51:32Z","page":"765 - 787","publication":"Acta Informatica","publisher":"Springer","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"Model checking the evolution of gene regulatory networks","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","call_identifier":"FP7","grant_number":"618091","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"name":"Limits to selection in biology and in evolutionary computation","call_identifier":"FP7","grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425"}],"isi":1,"author":[{"full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904","first_name":"Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","last_name":"Giacobbe"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","orcid":"0000-0001-6220-2052","first_name":"Calin C","full_name":"Guet, Calin C"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Paixao, Tiago","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","last_name":"Paixao","first_name":"Tiago","orcid":"0000-0003-2361-3953"},{"full_name":"Petrov, Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana","orcid":"0000-0002-9041-0905"}],"file":[{"content_type":"application/pdf","relation":"main_file","file_size":755241,"file_name":"2017_ActaInformatica_Giacobbe.pdf","date_updated":"2020-07-14T12:44:46Z","date_created":"2019-01-17T15:57:29Z","creator":"dernst","file_id":"5841","checksum":"4e661d9135d7f8c342e8e258dee76f3e","access_level":"open_access"}],"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"day":"01","citation":{"ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.","mla":"Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov, T. (2017). Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>","chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-016-0278-x\">https://doi.org/10.1007/s00236-016-0278-x</a>.","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787.","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking the evolution of gene regulatory networks,” <i>Acta Informatica</i>, vol. 54, no. 8. Springer, pp. 765–787, 2017.","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>. 2017;54(8):765-787. doi:<a href=\"https://doi.org/10.1007/s00236-016-0278-x\">10.1007/s00236-016-0278-x</a>"},"intvolume":"        54","scopus_import":"1","file_date_updated":"2020-07-14T12:44:46Z","ddc":["006","576"],"oa_version":"Published Version","date_published":"2017-12-01T00:00:00Z","publication_status":"published","doi":"10.1007/s00236-016-0278-x","month":"12","ec_funded":1,"status":"public","publication_identifier":{"issn":["00015903"]},"oa":1,"_id":"1351","date_updated":"2025-05-28T11:57:04Z","abstract":[{"lang":"eng","text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights."}],"issue":"8","year":"2017"}]