[{"scopus_import":"1","day":"09","article_type":"original","abstract":[{"lang":"eng","text":"In this work, we present hypernode automata as a specification formalism for hyperproperties of systems whose executions may be misaligned among themselves, such as concurrent systems. These automata consist of nodes labeled with hypernode logic formulas and transitions marked with synchronizing actions. Hypernode logic formulas establish relations between sequences of variable values among different system executions. This logic enables both synchronous and asynchronous analysis of traces. In its asynchronous view on execution traces, hypernode formulas establish relations on the order of value changes for each variable without correlating their timing. In both views, the analysis of different execution traces is synchronized through the transitions of hypernode automata. By combining logic’s declarative nature with automata’s procedural power, hypernode automata seamlessly integrate asynchronicity requirements at the node level with synchronicity between node transitions. We show that the model-checking problem for hypernode automata is decidable for specifications where each node specifies either a synchronous or an asynchronous requirement for the system’s executions, but not both."}],"volume":62,"project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"publication":"Acta Informatica","ddc":["000"],"ec_funded":1,"acknowledgement":"This work was supported in part by the Austrian Science Fund (FWF) SFB project SpyCoDe 10.55776/F85, by the FWF projects ZK-35 and W1255-N23, and by the ERC Advanced Grant VAMOS 101020093. Open access funding provided by Institute of Science and Technology (IST Austria).","issue":"4","language":[{"iso":"eng"}],"oa_version":"Published Version","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"citation":{"chicago":"Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>.","ieee":"E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” <i>Acta Informatica</i>, vol. 62, no. 4. Springer Nature, 2025.","short":"E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Acta Informatica 62 (2025).","apa":"Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Hypernode automata. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>","mla":"Bartocci, Ezio, et al. “Hypernode Automata.” <i>Acta Informatica</i>, vol. 62, no. 4, 43, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>.","ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43.","ama":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. <i>Acta Informatica</i>. 2025;62(4). doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>"},"file_date_updated":"2026-01-05T12:26:43Z","file":[{"date_updated":"2026-01-05T12:26:43Z","access_level":"open_access","success":1,"creator":"dernst","file_size":7117003,"file_id":"20944","relation":"main_file","date_created":"2026-01-05T12:26:43Z","file_name":"2025_ActaInformatica_Bartocci.pdf","checksum":"06ed45a1218ad8464818803ae2968aaf","content_type":"application/pdf"}],"has_accepted_license":"1","status":"public","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Hypernode automata","year":"2025","date_updated":"2026-01-05T12:27:41Z","doi":"10.1007/s00236-025-00509-8","_id":"20866","corr_author":"1","oa":1,"author":[{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","full_name":"Nickovic, Dejan","last_name":"Nickovic"},{"orcid":"0000-0002-8741-5799","first_name":"Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","full_name":"Oliveira da Costa, Ana","last_name":"Oliveira da Costa"}],"publisher":"Springer Nature","intvolume":"        62","fulldoi":"https://doi.org/10.1007/s00236-025-00509-8","arxiv":1,"related_material":{"record":[{"id":"14405","relation":"earlier_version","status":"public"}]},"date_published":"2025-12-09T00:00:00Z","type":"journal_article","external_id":{"arxiv":["2305.02836"]},"article_number":"43","date_created":"2025-12-29T12:07:12Z","publication_status":"published","OA_place":"publisher","month":"12","article_processing_charge":"Yes (via OA deal)","department":[{"_id":"ToHe"}],"OA_type":"hybrid"},{"date_published":"2025-09-01T00:00:00Z","type":"journal_article","fulldoi":"https://doi.org/10.1007/s00236-025-00502-1","department":[{"_id":"ToHe"}],"OA_type":"hybrid","OA_place":"publisher","month":"09","article_processing_charge":"Yes (via OA deal)","publication_status":"published","date_created":"2025-08-17T22:01:36Z","article_number":"30","external_id":{"isi":["001546115300001"]},"_id":"20186","PlanS_conform":"1","isi":1,"doi":"10.1007/s00236-025-00502-1","date_updated":"2025-09-30T14:20:11Z","year":"2025","title":"Gray-box runtime enforcement of hyperproperties","has_accepted_license":"1","quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","status":"public","intvolume":"        62","publisher":"Springer Nature","corr_author":"1","author":[{"last_name":"Hsu","full_name":"Hsu, Tzu Han","first_name":"Tzu Han"},{"last_name":"Oliveira Da Costa","full_name":"Oliveira Da Costa, Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","first_name":"Ana A"},{"first_name":"Andrew","full_name":"Wintenberg, Andrew","last_name":"Wintenberg"},{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"first_name":"Borzoo","full_name":"Bonakdarpour, Borzoo","last_name":"Bonakdarpour"}],"oa":1,"tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"oa_version":"Published Version","language":[{"iso":"eng"}],"issue":"3","acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018] (ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF) CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access funding provided by Institute of Science and Technology (IST Austria).","file":[{"content_type":"application/pdf","date_created":"2025-09-02T05:53:47Z","file_name":"2025_ActaInformatica_Hsu.pdf","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","creator":"dernst","file_size":6505049,"relation":"main_file","file_id":"20267","date_updated":"2025-09-02T05:53:47Z","access_level":"open_access","success":1}],"file_date_updated":"2025-09-02T05:53:47Z","citation":{"ista":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025. Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30.","mla":"Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>, vol. 62, no. 3, 30, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>.","ama":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. 2025;62(3). doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>","chicago":"Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>.","ieee":"T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour, “Gray-box runtime enforcement of hyperproperties,” <i>Acta Informatica</i>, vol. 62, no. 3. Springer Nature, 2025.","apa":"Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., &#38; Bonakdarpour, B. (2025). Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025)."},"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"volume":62,"abstract":[{"text":"Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of hyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants.","lang":"eng"}],"day":"01","article_type":"original","scopus_import":"1","ddc":["000"],"publication":"Acta Informatica"},{"page":"585-618","ddc":["000"],"publication":"Acta Informatica","article_type":"original","day":"01","scopus_import":"1","volume":59,"abstract":[{"lang":"eng","text":"Transforming ω-automata into parity automata is traditionally done using appearance records. We present an efficient variant of this idea, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and show that our method produces significantly smaller automata than previous approaches."}],"project":[{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"keyword":["computer networks and communications","information systems","software"],"citation":{"ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","mla":"Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>, vol. 59, Springer Nature, 2022, pp. 585–618, doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>.","ama":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record with preorders. <i>Acta Informatica</i>. 2022;59:585-618. doi:<a href=\"https://doi.org/10.1007/s00236-021-00412-y\">10.1007/s00236-021-00412-y</a>","chicago":"Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record with Preorders.” <i>Acta Informatica</i>. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>.","ieee":"J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record with preorders,” <i>Acta Informatica</i>, vol. 59. Springer Nature, pp. 585–618, 2022.","apa":"Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2022). Index appearance record with preorders. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-021-00412-y\">https://doi.org/10.1007/s00236-021-00412-y</a>","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618."},"file_date_updated":"2022-01-07T07:50:31Z","file":[{"date_created":"2022-01-07T07:50:31Z","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","file_name":"2021_ActaInfor_Křetínský.pdf","content_type":"application/pdf","date_updated":"2022-01-07T07:50:31Z","success":1,"access_level":"open_access","creator":"cchlebak","relation":"main_file","file_id":"10603","file_size":1066082}],"acknowledgement":"This work is partially funded by the German Research Foundation (DFG) projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification (No. 383882557), and the Alexander von Humboldt Foundation with funds from the German Federal Ministry of Education and Research. It is an extended version of [21], including all proofs together with further explanations and examples. Moreover, we provide a new, more efficient construction based on (total) preorders, unifying previous optimizations. Experiments are performed with a new, performant implementation, comparing our approach to the current state of the art.","language":[{"iso":"eng"}],"tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"oa_version":"Published Version","oa":1,"corr_author":"1","author":[{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer","orcid":"0000-0002-1712-2165","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","first_name":"Tobias"},{"first_name":"Clara","last_name":"Waldmann","full_name":"Waldmann, Clara"},{"first_name":"Maximilian","last_name":"Weininger","full_name":"Weininger, Maximilian"}],"publisher":"Springer Nature","intvolume":"        59","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","quality_controlled":"1","has_accepted_license":"1","doi":"10.1007/s00236-021-00412-y","year":"2022","title":"Index appearance record with preorders","date_updated":"2025-04-15T06:53:08Z","isi":1,"_id":"10602","external_id":{"isi":["000735765500001"]},"date_created":"2022-01-06T12:37:27Z","publication_status":"published","department":[{"_id":"KrCh"}],"month":"10","article_processing_charge":"Yes (via OA deal)","fulldoi":"https://doi.org/10.1007/s00236-021-00412-y","date_published":"2022-10-01T00:00:00Z","type":"journal_article"},{"date_published":"2017-12-01T00:00:00Z","type":"journal_article","related_material":{"record":[{"relation":"earlier_version","id":"1835","status":"public"}]},"fulldoi":"https://doi.org/10.1007/s00236-016-0278-x","month":"12","article_processing_charge":"No","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"publication_status":"published","date_created":"2018-12-11T11:51:32Z","external_id":{"isi":["000414343200003"]},"isi":1,"_id":"1351","year":"2017","title":"Model checking the evolution of gene regulatory networks","date_updated":"2025-07-10T11:50:42Z","doi":"10.1007/s00236-016-0278-x","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","quality_controlled":"1","has_accepted_license":"1","publisher":"Springer","intvolume":"        54","publist_id":"5898","corr_author":"1","oa":1,"author":[{"orcid":"0000-0001-8180-0904","first_name":"Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","full_name":"Giacobbe, Mirco","last_name":"Giacobbe"},{"orcid":"0000-0001-6220-2052","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C","last_name":"Guet"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Paixao, Tiago","last_name":"Paixao","orcid":"0000-0003-2361-3953","first_name":"Tiago","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Tatjana","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905","last_name":"Petrov","full_name":"Petrov, Tatjana"}],"oa_version":"Published Version","tmp":{"short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"issue":"8","pubrep_id":"649","file":[{"content_type":"application/pdf","date_created":"2019-01-17T15:57:29Z","file_name":"2017_ActaInformatica_Giacobbe.pdf","checksum":"4e661d9135d7f8c342e8e258dee76f3e","creator":"dernst","file_size":755241,"file_id":"5841","relation":"main_file","date_updated":"2020-07-14T12:44:46Z","access_level":"open_access"}],"file_date_updated":"2020-07-14T12:44:46Z","citation":{"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>.","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.","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787.","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>","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>.","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.","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>"},"publication_identifier":{"issn":["0001-5903"]},"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","grant_number":"618091","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"},{"call_identifier":"FP7","grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation","_id":"25B07788-B435-11E9-9278-68D0E5697425"}],"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."}],"volume":54,"scopus_import":"1","day":"01","ec_funded":1,"publication":"Acta Informatica","ddc":["006","576"],"page":"765 - 787"},{"publication_status":"published","month":"09","article_processing_charge":"No","department":[{"_id":"KrCh"}],"external_id":{"isi":["000407713300001"]},"date_created":"2018-12-11T11:48:07Z","type":"journal_article","date_published":"2017-09-01T00:00:00Z","fulldoi":"https://doi.org/10.1007/s00236-017-0299-0","corr_author":"1","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Rüdiger","last_name":"Ehlers","full_name":"Ehlers, Rüdiger"}],"publisher":"Springer","intvolume":"        54","publist_id":"6961","_id":"719","isi":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","status":"public","quality_controlled":"1","date_updated":"2025-09-10T10:59:19Z","year":"2017","title":"Special issue: Synthesis and SYNT 2014","doi":"10.1007/s00236-017-0299-0","publication_identifier":{"issn":["0001-5903"]},"citation":{"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.","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>.","short":"K. Chatterjee, R. Ehlers, Acta Informatica 54 (2017) 543–544.","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>"},"oa_version":"None","issue":"6","language":[{"iso":"eng"}],"page":"543 - 544","publication":"Acta Informatica","scopus_import":"1","day":"01","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."}],"volume":54}]