[{"volume":62,"ddc":["000"],"fulldoi":"https://doi.org/10.1007/s00236-025-00509-8","related_material":{"record":[{"relation":"earlier_version","id":"14405","status":"public"}]},"intvolume":"        62","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).","language":[{"iso":"eng"}],"abstract":[{"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.","lang":"eng"}],"doi":"10.1007/s00236-025-00509-8","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"status":"public","has_accepted_license":"1","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"issue":"4","citation":{"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>","ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43.","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>.","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.","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>","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>.","short":"E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Acta Informatica 62 (2025)."},"day":"09","external_id":{"arxiv":["2305.02836"]},"oa_version":"Published Version","article_processing_charge":"Yes (via OA deal)","date_updated":"2026-01-05T12:27:41Z","month":"12","arxiv":1,"date_created":"2025-12-29T12:07:12Z","article_type":"original","title":"Hypernode automata","_id":"20866","ec_funded":1,"publication":"Acta Informatica","file":[{"relation":"main_file","checksum":"06ed45a1218ad8464818803ae2968aaf","creator":"dernst","file_name":"2025_ActaInformatica_Bartocci.pdf","content_type":"application/pdf","access_level":"open_access","date_created":"2026-01-05T12:26:43Z","file_size":7117003,"date_updated":"2026-01-05T12:26:43Z","success":1,"file_id":"20944"}],"author":[{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nickovic","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan"},{"first_name":"Ana","orcid":"0000-0002-8741-5799","last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4"}],"date_published":"2025-12-09T00:00:00Z","department":[{"_id":"ToHe"}],"OA_type":"hybrid","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"},{"name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502"}],"type":"journal_article","scopus_import":"1","year":"2025","corr_author":"1","quality_controlled":"1","article_number":"43","oa":1,"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2026-01-05T12:26:43Z","publisher":"Springer Nature","publication_status":"published"},{"article_processing_charge":"Yes (via OA deal)","month":"09","date_updated":"2025-09-30T14:20:11Z","date_created":"2025-08-17T22:01:36Z","title":"Gray-box runtime enforcement of hyperproperties","article_type":"original","_id":"20186","file":[{"access_level":"open_access","content_type":"application/pdf","creator":"dernst","file_name":"2025_ActaInformatica_Hsu.pdf","relation":"main_file","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","date_updated":"2025-09-02T05:53:47Z","file_id":"20267","success":1,"file_size":6505049,"date_created":"2025-09-02T05:53:47Z"}],"publication":"Acta Informatica","date_published":"2025-09-01T00:00:00Z","author":[{"full_name":"Hsu, Tzu Han","last_name":"Hsu","first_name":"Tzu Han"},{"full_name":"Oliveira Da Costa, Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","first_name":"Ana A","last_name":"Oliveira Da Costa"},{"full_name":"Wintenberg, Andrew","first_name":"Andrew","last_name":"Wintenberg"},{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"full_name":"Bonakdarpour, Borzoo","first_name":"Borzoo","last_name":"Bonakdarpour"}],"project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"OA_type":"hybrid","department":[{"_id":"ToHe"}],"corr_author":"1","year":"2025","scopus_import":"1","type":"journal_article","OA_place":"publisher","oa":1,"quality_controlled":"1","article_number":"30","file_date_updated":"2025-09-02T05:53:47Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication_status":"published","publisher":"Springer Nature","volume":62,"ddc":["000"],"PlanS_conform":"1","fulldoi":"https://doi.org/10.1007/s00236-025-00502-1","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).","intvolume":"        62","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","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."}],"isi":1,"doi":"10.1007/s00236-025-00502-1","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"has_accepted_license":"1","status":"public","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"issue":"3","citation":{"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>","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025).","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.","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>.","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.","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>"},"day":"01","oa_version":"Published Version","external_id":{"isi":["001546115300001"]}},{"_id":"10602","date_published":"2022-10-01T00:00:00Z","author":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan"},{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","first_name":"Tobias"},{"full_name":"Waldmann, Clara","first_name":"Clara","last_name":"Waldmann"},{"first_name":"Maximilian","last_name":"Weininger","full_name":"Weininger, Maximilian"}],"file":[{"file_size":1066082,"date_created":"2022-01-07T07:50:31Z","file_id":"10603","success":1,"date_updated":"2022-01-07T07:50:31Z","file_name":"2021_ActaInfor_Křetínský.pdf","creator":"cchlebak","relation":"main_file","checksum":"bf1c195b6aaf59e8530cf9e3a9d731f7","access_level":"open_access","content_type":"application/pdf"}],"publication":"Acta Informatica","month":"10","date_updated":"2025-04-15T06:53:08Z","article_processing_charge":"Yes (via OA deal)","title":"Index appearance record with preorders","article_type":"original","date_created":"2022-01-06T12:37:27Z","quality_controlled":"1","oa":1,"publication_status":"published","publisher":"Springer Nature","file_date_updated":"2022-01-07T07:50:31Z","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","page":"585-618","corr_author":"1","scopus_import":"1","year":"2022","type":"journal_article","project":[{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"department":[{"_id":"KrCh"}],"abstract":[{"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.","lang":"eng"}],"isi":1,"language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"doi":"10.1007/s00236-021-00412-y","ddc":["000"],"volume":59,"intvolume":"        59","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.","fulldoi":"https://doi.org/10.1007/s00236-021-00412-y","citation":{"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>","short":"J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica 59 (2022) 585–618.","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.","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>.","ista":"Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance record with preorders. Acta Informatica. 59, 585–618.","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>"},"oa_version":"Published Version","keyword":["computer networks and communications","information systems","software"],"external_id":{"isi":["000735765500001"]},"day":"01","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","has_accepted_license":"1"},{"file_date_updated":"2020-07-14T12:44:46Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"765 - 787","publication_status":"published","publisher":"Springer","quality_controlled":"1","oa":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"},{"name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","call_identifier":"FP7","grant_number":"618091","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"},{"name":"Limits to selection in biology and in evolutionary computation","call_identifier":"FP7","grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"corr_author":"1","scopus_import":"1","year":"2017","type":"journal_article","publication":"Acta Informatica","file":[{"content_type":"application/pdf","access_level":"open_access","checksum":"4e661d9135d7f8c342e8e258dee76f3e","relation":"main_file","creator":"dernst","file_name":"2017_ActaInformatica_Giacobbe.pdf","file_id":"5841","date_updated":"2020-07-14T12:44:46Z","date_created":"2019-01-17T15:57:29Z","file_size":755241}],"date_published":"2017-12-01T00:00:00Z","author":[{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","full_name":"Giacobbe, Mirco","last_name":"Giacobbe","orcid":"0000-0001-8180-0904","first_name":"Mirco"},{"orcid":"0000-0001-6220-2052","last_name":"Guet","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","full_name":"Guet, Calin C"},{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","full_name":"Paixao, Tiago","last_name":"Paixao","orcid":"0000-0003-2361-3953","first_name":"Tiago"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","last_name":"Petrov","first_name":"Tatjana"}],"pubrep_id":"649","ec_funded":1,"_id":"1351","date_created":"2018-12-11T11:51:32Z","title":"Model checking the evolution of gene regulatory networks","article_processing_charge":"No","publist_id":"5898","month":"12","date_updated":"2025-07-10T11:50:42Z","day":"01","oa_version":"Published Version","external_id":{"isi":["000414343200003"]},"issue":"8","citation":{"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>.","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>.","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>","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.","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>","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."},"has_accepted_license":"1","status":"public","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"doi":"10.1007/s00236-016-0278-x","publication_identifier":{"issn":["0001-5903"]},"language":[{"iso":"eng"}],"abstract":[{"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.","lang":"eng"}],"isi":1,"related_material":{"record":[{"id":"1835","relation":"earlier_version","status":"public"}]},"fulldoi":"https://doi.org/10.1007/s00236-016-0278-x","intvolume":"        54","volume":54,"ddc":["006","576"]},{"isi":1,"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."}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0001-5903"]},"doi":"10.1007/s00236-017-0299-0","volume":54,"intvolume":"        54","fulldoi":"https://doi.org/10.1007/s00236-017-0299-0","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>.","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>","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.","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.","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>","ista":"Chatterjee K, Ehlers R. 2017. Special issue: Synthesis and SYNT 2014. Acta Informatica. 54(6), 543–544."},"issue":"6","external_id":{"isi":["000407713300001"]},"oa_version":"None","day":"01","status":"public","_id":"719","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Ehlers, Rüdiger","first_name":"Rüdiger","last_name":"Ehlers"}],"date_published":"2017-09-01T00:00:00Z","publication":"Acta Informatica","publist_id":"6961","month":"09","date_updated":"2025-09-10T10:59:19Z","article_processing_charge":"No","title":"Special issue: Synthesis and SYNT 2014","date_created":"2018-12-11T11:48:07Z","quality_controlled":"1","publisher":"Springer","publication_status":"published","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","page":"543 - 544","type":"journal_article","scopus_import":"1","year":"2017","corr_author":"1","department":[{"_id":"KrCh"}]}]