[{"abstract":[{"lang":"eng","text":"Gene expression is regulated by the set of transcription factors (TFs) that bind to the promoter. The ensuing regulating function is often represented as a combinational logic circuit, where output (gene expression) is determined by current input values (promoter bound TFs) only. However, the simultaneous arrival of TFs is a strong assumption, since transcription and translation of genes introduce intrinsic time delays and there is no global synchronisation among the arrival times of different molecular species at their targets. We present an experimentally implementable genetic circuit with two inputs and one output, which in the presence of small delays in input arrival, exhibits qualitatively distinct population-level phenotypes, over timescales that are longer than typical cell doubling times. From a dynamical systems point of view, these phenotypes represent long-lived transients: although they converge to the same value eventually, they do so after a very long time span. The key feature of this toy model genetic circuit is that, despite having only two inputs and one output, it is regulated by twenty-three distinct DNA-TF configurations, two of which are more stable than others (DNA looped states), one promoting and another blocking the expression of the output gene. Small delays in input arrival time result in a majority of cells in the population quickly reaching the stable state associated with the first input, while exiting of this stable state occurs at a slow timescale. In order to mechanistically model the behaviour of this genetic circuit, we used a rule-based modelling language, and implemented a grid-search to find parameter combinations giving rise to long-lived transients. Our analysis shows that in the absence of feedback, there exist path-dependent gene regulatory mechanisms based on the long timescale of transients. The behaviour of this toy model circuit suggests that gene regulatory networks can exploit event timing to create phenotypes, and it opens the possibility that they could use event timing to memorise events, without regulatory feedback. The model reveals the importance of (i) mechanistically modelling the transitions between the different DNA-TF states, and (ii) employing transient analysis thereof."}],"oa_version":"Published Version","scopus_import":"1","intvolume":" 893","month":"06","publication_status":"published","publication_identifier":{"issn":["0304-3975"]},"language":[{"iso":"eng"}],"file":[{"success":1,"file_id":"11364","checksum":"d3aef34cfb13e53bba4cf44d01680793","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"2021_TheoreticalComputerScience_Petrov.pdf","date_created":"2022-05-12T12:13:27Z","file_size":2566504,"date_updated":"2022-05-12T12:13:27Z","creator":"dernst"}],"license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","volume":893,"_id":"9647","tmp":{"short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png"},"type":"journal_article","article_type":"original","status":"public","date_updated":"2023-08-10T14:11:19Z","ddc":["004"],"department":[{"_id":"ToHe"},{"_id":"CaGu"}],"file_date_updated":"2022-05-12T12:13:27Z","acknowledgement":"Tatjana Petrov’s research was supported in part by SNSF Advanced Postdoctoral Mobility Fellowship grant number P300P2 161067, the Ministry of Science, Research and the Arts of the state of Baden-Wurttemberg, and the DFG Centre of Excellence 2117 ‘Centre for the Advanced Study of Collective Behaviour’ (ID: 422037984). Claudia Igler is the recipient of a DOC Fellowship of the Austrian Academy of Sciences. Thomas A. Henzinger’s research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","oa":1,"publisher":"Elsevier","quality_controlled":"1","year":"2021","isi":1,"has_accepted_license":"1","publication":"Theoretical Computer Science","day":"04","page":"1-16","date_created":"2021-07-11T22:01:18Z","date_published":"2021-06-04T00:00:00Z","doi":"10.1016/j.tcs.2021.05.023","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"citation":{"mla":"Petrov, Tatjana, et al. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science, vol. 893, Elsevier, 2021, pp. 1–16, doi:10.1016/j.tcs.2021.05.023.","short":"T. Petrov, C. Igler, A. Sezgin, T.A. Henzinger, C.C. Guet, Theoretical Computer Science 893 (2021) 1–16.","ieee":"T. Petrov, C. Igler, A. Sezgin, T. A. Henzinger, and C. C. Guet, “Long lived transients in gene regulation,” Theoretical Computer Science, vol. 893. Elsevier, pp. 1–16, 2021.","ama":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. Long lived transients in gene regulation. Theoretical Computer Science. 2021;893:1-16. doi:10.1016/j.tcs.2021.05.023","apa":"Petrov, T., Igler, C., Sezgin, A., Henzinger, T. A., & Guet, C. C. (2021). Long lived transients in gene regulation. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2021.05.023","chicago":"Petrov, Tatjana, Claudia Igler, Ali Sezgin, Thomas A Henzinger, and Calin C Guet. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science. Elsevier, 2021. https://doi.org/10.1016/j.tcs.2021.05.023.","ista":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. 2021. Long lived transients in gene regulation. Theoretical Computer Science. 893, 1–16."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","article_processing_charge":"No","external_id":{"isi":["000710180500002"]},"author":[{"first_name":"Tatjana","full_name":"Petrov, Tatjana","last_name":"Petrov"},{"full_name":"Igler, Claudia","last_name":"Igler","first_name":"Claudia","id":"46613666-F248-11E8-B48F-1D18A9856A87"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","full_name":"Sezgin, Ali","last_name":"Sezgin"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Guet","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","first_name":"Calin C"}],"title":"Long lived transients in gene regulation"},{"type":"journal_article","article_type":"original","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","_id":"9761","file_date_updated":"2021-08-04T14:01:30Z","department":[{"_id":"SaSi"}],"date_updated":"2023-08-10T14:14:53Z","ddc":["570"],"scopus_import":"1","month":"06","intvolume":" 10","abstract":[{"lang":"eng","text":"The important roles of mitochondrial function and dysfunction in the process of neurodegeneration are widely acknowledged. Retinal ganglion cells (RGCs) appear to be a highly vulnerable neuronal cell type in the central nervous system with respect to mitochondrial dysfunction but the actual reasons for this are still incompletely understood. These cells have a unique circumstance where unmyelinated axons must bend nearly 90° to exit the eye and then cross a translaminar pressure gradient before becoming myelinated in the optic nerve. This region, the optic nerve head, contains some of the highest density of mitochondria present in these cells. Glaucoma represents a perfect storm of events occurring at this location, with a combination of changes in the translaminar pressure gradient and reassignment of the metabolic support functions of supporting glia, which appears to apply increased metabolic stress to the RGC axons leading to a failure of axonal transport mechanisms. However, RGCs themselves are also extremely sensitive to genetic mutations, particularly in genes affecting mitochondrial dynamics and mitochondrial clearance. These mutations, which systemically affect the mitochondria in every cell, often lead to an optic neuropathy as the sole pathologic defect in affected patients. This review summarizes knowledge of mitochondrial structure and function, the known energy demands of neurons in general, and places these in the context of normal and pathological characteristics of mitochondria attributed to RGCs. "}],"oa_version":"Published Version","pmid":1,"issue":"7","volume":10,"license":"https://creativecommons.org/licenses/by/4.0/","publication_identifier":{"eissn":["20734409"]},"publication_status":"published","file":[{"success":1,"checksum":"e0497ce5c77fa3b65a538c7d6e0f6c66","file_id":"9768","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2021_Cells_Muench.pdf","date_created":"2021-08-04T14:01:30Z","creator":"cziletti","file_size":4555611,"date_updated":"2021-08-04T14:01:30Z"}],"language":[{"iso":"eng"}],"article_number":"1593","author":[{"first_name":"Nicole A.","last_name":"Muench","full_name":"Muench, Nicole A."},{"full_name":"Patel, Sonia","last_name":"Patel","first_name":"Sonia"},{"id":"3838F452-F248-11E8-B48F-1D18A9856A87","first_name":"Margaret E","full_name":"Maes, Margaret E","orcid":"0000-0001-9642-1085","last_name":"Maes"},{"first_name":"Ryan J.","last_name":"Donahue","full_name":"Donahue, Ryan J."},{"first_name":"Akihiro","full_name":"Ikeda, Akihiro","last_name":"Ikeda"},{"full_name":"Nickells, Robert W.","last_name":"Nickells","first_name":"Robert W."}],"external_id":{"pmid":["34201955"],"isi":["000678193300001"]},"article_processing_charge":"Yes","title":"The influence of mitochondrial dynamics and function on retinal ganglion cell susceptibility in optic nerve disease","citation":{"ista":"Muench NA, Patel S, Maes ME, Donahue RJ, Ikeda A, Nickells RW. 2021. The influence of mitochondrial dynamics and function on retinal ganglion cell susceptibility in optic nerve disease. Cells. 10(7), 1593.","chicago":"Muench, Nicole A., Sonia Patel, Margaret E Maes, Ryan J. Donahue, Akihiro Ikeda, and Robert W. Nickells. “The Influence of Mitochondrial Dynamics and Function on Retinal Ganglion Cell Susceptibility in Optic Nerve Disease.” Cells. MDPI, 2021. https://doi.org/10.3390/cells10071593.","short":"N.A. Muench, S. Patel, M.E. Maes, R.J. Donahue, A. Ikeda, R.W. Nickells, Cells 10 (2021).","ieee":"N. A. Muench, S. Patel, M. E. Maes, R. J. Donahue, A. Ikeda, and R. W. Nickells, “The influence of mitochondrial dynamics and function on retinal ganglion cell susceptibility in optic nerve disease,” Cells, vol. 10, no. 7. MDPI, 2021.","ama":"Muench NA, Patel S, Maes ME, Donahue RJ, Ikeda A, Nickells RW. The influence of mitochondrial dynamics and function on retinal ganglion cell susceptibility in optic nerve disease. Cells. 2021;10(7). doi:10.3390/cells10071593","apa":"Muench, N. A., Patel, S., Maes, M. E., Donahue, R. J., Ikeda, A., & Nickells, R. W. (2021). The influence of mitochondrial dynamics and function on retinal ganglion cell susceptibility in optic nerve disease. Cells. MDPI. https://doi.org/10.3390/cells10071593","mla":"Muench, Nicole A., et al. “The Influence of Mitochondrial Dynamics and Function on Retinal Ganglion Cell Susceptibility in Optic Nerve Disease.” Cells, vol. 10, no. 7, 1593, MDPI, 2021, doi:10.3390/cells10071593."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","quality_controlled":"1","publisher":"MDPI","oa":1,"acknowledgement":"The authors are grateful to Kazuya Oikawa and Gillian McLellan for generously sharing some of their data for this review, and to Janis Eells for helpful comments on the manuscript.","date_published":"2021-06-25T00:00:00Z","doi":"10.3390/cells10071593","date_created":"2021-08-01T22:01:22Z","isi":1,"has_accepted_license":"1","year":"2021","day":"25","publication":"Cells"},{"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ista":"Fredes F, Shigemoto R. 2021. The role of hippocampal mossy cells in novelty detection. Neurobiology of Learning and Memory. 183, 107486.","chicago":"Fredes, Felipe, and Ryuichi Shigemoto. “The Role of Hippocampal Mossy Cells in Novelty Detection.” Neurobiology of Learning and Memory. Elsevier, 2021. https://doi.org/10.1016/j.nlm.2021.107486.","apa":"Fredes, F., & Shigemoto, R. (2021). The role of hippocampal mossy cells in novelty detection. Neurobiology of Learning and Memory. Elsevier. https://doi.org/10.1016/j.nlm.2021.107486","ama":"Fredes F, Shigemoto R. The role of hippocampal mossy cells in novelty detection. Neurobiology of Learning and Memory. 2021;183. doi:10.1016/j.nlm.2021.107486","short":"F. Fredes, R. Shigemoto, Neurobiology of Learning and Memory 183 (2021).","ieee":"F. Fredes and R. Shigemoto, “The role of hippocampal mossy cells in novelty detection,” Neurobiology of Learning and Memory, vol. 183. Elsevier, 2021.","mla":"Fredes, Felipe, and Ryuichi Shigemoto. “The Role of Hippocampal Mossy Cells in Novelty Detection.” Neurobiology of Learning and Memory, vol. 183, 107486, Elsevier, 2021, doi:10.1016/j.nlm.2021.107486."},"title":"The role of hippocampal mossy cells in novelty detection","external_id":{"pmid":["34214666"],"isi":["000677694900004"]},"article_processing_charge":"No","author":[{"first_name":"Felipe","full_name":"Fredes, Felipe","last_name":"Fredes"},{"orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi","last_name":"Shigemoto","first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87"}],"article_number":"107486","project":[{"_id":"25CA28EA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"In situ analysis of single channel subunit composition in neurons: physiological implication in synaptic plasticity and behaviour","grant_number":"694539"}],"publication":"Neurobiology of Learning and Memory","day":"30","year":"2021","has_accepted_license":"1","isi":1,"date_created":"2021-07-11T22:01:16Z","doi":"10.1016/j.nlm.2021.107486","date_published":"2021-06-30T00:00:00Z","acknowledgement":"This work was supported by a European Research Council Advanced Grant 694539 to Ryuichi Shigemoto.","oa":1,"publisher":"Elsevier","quality_controlled":"1","ddc":["610"],"date_updated":"2023-08-10T14:10:37Z","department":[{"_id":"RySh"}],"file_date_updated":"2021-07-19T13:46:06Z","_id":"9641","status":"public","tmp":{"short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png"},"article_type":"original","type":"journal_article","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"8e8298a9e8c7df146ad23f32c2a63929","file_id":"9694","success":1,"date_updated":"2021-07-19T13:46:06Z","file_size":1994793,"creator":"cziletti","date_created":"2021-07-19T13:46:06Z","file_name":"2021_NeurobLearnMemory_Fredes.pdf"}],"publication_status":"published","publication_identifier":{"eissn":["10959564"],"issn":["10747427"]},"ec_funded":1,"volume":183,"oa_version":"Published Version","pmid":1,"abstract":[{"text":"At the encounter with a novel environment, contextual memory formation is greatly enhanced, accompanied with increased arousal and active exploration. Although this phenomenon has been widely observed in animal and human daily life, how the novelty in the environment is detected and contributes to contextual memory formation has lately started to be unveiled. The hippocampus has been studied for many decades for its largely known roles in encoding spatial memory, and a growing body of evidence indicates a differential involvement of dorsal and ventral hippocampal divisions in novelty detection. In this brief review article, we discuss the recent findings of the role of mossy cells in the ventral hippocampal moiety in novelty detection and put them in perspective with other novelty-related pathways in the hippocampus. We propose a mechanism for novelty-driven memory acquisition in the dentate gyrus by the direct projection of ventral mossy cells to dorsal dentate granule cells. By this projection, the ventral hippocampus sends novelty signals to the dorsal hippocampus, opening a gate for memory encoding in dentate granule cells based on information coming from the entorhinal cortex. We conclude that, contrary to the presently accepted functional independence, the dorsal and ventral hippocampi cooperate to link the novelty and contextual information, and this dorso-ventral interaction is crucial for the novelty-dependent memory formation.","lang":"eng"}],"intvolume":" 183","month":"06","scopus_import":"1"},{"department":[{"_id":"KrCh"}],"date_updated":"2023-08-10T14:14:08Z","conference":{"start_date":"2021-06-20","end_date":"2021-06-26","location":"Online","name":"PLDI: Programming Language Design and Implementation"},"type":"conference","status":"public","_id":"9646","ec_funded":1,"publication_status":"published","publication_identifier":{"isbn":["9781450383912"]},"language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/2011.14617","open_access":"1"}],"scopus_import":"1","month":"06","abstract":[{"lang":"eng","text":"We consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking supermartingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approaches. On the practical side, we show our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are remarkably tighter than previous results, in some cases by thousands of orders of magnitude."}],"oa_version":"Preprint","article_processing_charge":"No","external_id":{"isi":["000723661700076"],"arxiv":["2011.14617"]},"author":[{"first_name":"Jinyi","full_name":"Wang, Jinyi","last_name":"Wang"},{"first_name":"Yican","last_name":"Sun","full_name":"Sun, Yican"},{"first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu","full_name":"Fu, Hongfei"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584"}],"title":"Quantitative analysis of assertion violations in probabilistic programs","citation":{"chicago":"Wang, Jinyi, Yican Sun, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 1171–86. Association for Computing Machinery, 2021. https://doi.org/10.1145/3453483.3454102.","ista":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. 2021. Quantitative analysis of assertion violations in probabilistic programs. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1171–1186.","mla":"Wang, Jinyi, et al. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.” Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1171–86, doi:10.1145/3453483.3454102.","short":"J. Wang, Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1171–1186.","ieee":"J. Wang, Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Quantitative analysis of assertion violations in probabilistic programs,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Online, 2021, pp. 1171–1186.","ama":"Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. Quantitative analysis of assertion violations in probabilistic programs. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2021:1171-1186. doi:10.1145/3453483.3454102","apa":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., & Goharshady, A. K. (2021). Quantitative analysis of assertion violations in probabilistic programs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 1171–1186). Online: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454102"},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"page":"1171-1186","date_created":"2021-07-11T22:01:18Z","doi":"10.1145/3453483.3454102","date_published":"2021-06-01T00:00:00Z","year":"2021","isi":1,"publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","day":"01","oa":1,"publisher":"Association for Computing Machinery","quality_controlled":"1","acknowledgement":"We are very thankful to the anonymous reviewers for the helpful and valuable comments. The work was partially supported by the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research Program, the ERC CoG 863818 (ForM-SMArt), the Facebook PhD Fellowship Program and DOC Fellowship #24956 of the Austrian Academy of Sciences (ÖAW)."},{"department":[{"_id":"KrCh"}],"date_updated":"2023-08-10T14:13:39Z","conference":{"end_date":"2021-06-26","location":"Online","start_date":"2021-06-20","name":" PLDI: Programming Language Design and Implementation"},"type":"conference","status":"public","_id":"9645","ec_funded":1,"publication_status":"published","publication_identifier":{"isbn":["9781450383912"]},"language":[{"iso":"eng"}],"main_file_link":[{"url":"https://hal.archives-ouvertes.fr/hal-03183862/","open_access":"1"}],"scopus_import":"1","month":"06","abstract":[{"lang":"eng","text":"We consider the fundamental problem of reachability analysis over imperative programs with real variables. Previous works that tackle reachability are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic). In contrast, we propose a novel approach for reachability analysis that can handle general and complex loops, is complete, and can be entirely automated for a wide family of programs. Through the notion of Inductive Reachability Witnesses (IRWs), our approach extends ideas from both invariant generation and termination to reachability analysis.\r\n\r\nWe first show that our IRW-based approach is sound and complete for reachability analysis of imperative programs. Then, we focus on linear and polynomial programs and develop automated methods for synthesizing linear and polynomial IRWs. In the linear case, we follow the well-known approaches using Farkas' Lemma. Our main contribution is in the polynomial case, where we present a push-button semi-complete algorithm. We achieve this using a novel combination of classical theorems in real algebraic geometry, such as Putinar's Positivstellensatz and Hilbert's Strong Nullstellensatz. Finally, our experimental results show we can prove complex reachability objectives over various benchmarks that were beyond the reach of previous methods."}],"oa_version":"Submitted Version","external_id":{"isi":["000723661700050"]},"article_processing_charge":"No","author":[{"first_name":"Ali","full_name":"Asadi, Ali","last_name":"Asadi"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei","last_name":"Fu"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady"},{"last_name":"Mahdavi","full_name":"Mahdavi, Mohammad","first_name":"Mohammad"}],"title":"Polynomial reachability witnesses via Stellensätze","citation":{"ieee":"A. Asadi, K. Chatterjee, H. Fu, A. K. Goharshady, and M. Mahdavi, “Polynomial reachability witnesses via Stellensätze,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Online, 2021, pp. 772–787.","short":"A. Asadi, K. Chatterjee, H. Fu, A.K. Goharshady, M. Mahdavi, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 772–787.","ama":"Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. Polynomial reachability witnesses via Stellensätze. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2021:772-787. doi:10.1145/3453483.3454076","apa":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A. K., & Mahdavi, M. (2021). Polynomial reachability witnesses via Stellensätze. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 772–787). Online: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454076","mla":"Asadi, Ali, et al. “Polynomial Reachability Witnesses via Stellensätze.” Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 772–87, doi:10.1145/3453483.3454076.","ista":"Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. 2021. Polynomial reachability witnesses via Stellensätze. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 772–787.","chicago":"Asadi, Ali, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. “Polynomial Reachability Witnesses via Stellensätze.” In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 772–87. Association for Computing Machinery, 2021. https://doi.org/10.1145/3453483.3454076."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"},{"_id":"267066CE-B435-11E9-9278-68D0E5697425","name":"Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies"}],"page":"772-787","date_created":"2021-07-11T22:01:17Z","date_published":"2021-06-01T00:00:00Z","doi":"10.1145/3453483.3454076","year":"2021","isi":1,"publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","day":"01","oa":1,"publisher":"Association for Computing Machinery","quality_controlled":"1","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research Program, the Facebook PhD Fellowship Program, and DOC Fellowship No. 24956 of the Austrian Academy of Sciences (ÖAW)."}]