{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T20:30:19Z","timestamp":1792787419598,"version":"4.5.0"},"reference-count":194,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2022,12,7]],"date-time":"2022-12-07T00:00:00Z","timestamp":1670371200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR-NRF French-Singaporean research program ProMiS","award":["ANR-19-CE25-0015"],"award-info":[{"award-number":["ANR-19-CE25-0015"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2023,7,31]]},"abstract":"<jats:p>\n                    Timed automata are a common formalism for the verification of concurrent systems subject to timing constraints. They extend finite-state automata with clocks, that constrain the system behavior in locations, and to take transitions. While timed automata were originally designed for\n                    <jats:italic>safety<\/jats:italic>\n                    (in the wide sense of correctness w.r.t. a formal property), they were progressively used in a number of works to guarantee\n                    <jats:italic>security<\/jats:italic>\n                    properties. In this work, we review works studying security properties for timed automata over the past two decades. We notably review theoretical works, with a particular focus on opacity, as well as more practical works, with a particular focus on attack trees and their extensions. We derive main conclusions concerning open perspectives, as well as tool support.\n                  <\/jats:p>","DOI":"10.1145\/3534967","type":"journal-article","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T08:53:49Z","timestamp":1652950429000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Timed Automata as a Formalism for Expressing Security: A Survey on Theory and Practice"],"prefix":"10.1145","volume":"55","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9979-3829","authenticated-orcid":false,"given":"Johan","family":"Arcile","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, Nancy, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8473-9555","authenticated-orcid":false,"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, Nancy, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,12,7]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"[n.d.]. Uppaal CORA. Retrieved from https:\/\/docs.uppaal.org\/extensions\/cora\/."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.07.048"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00330-9"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/FUZZY.2010.5584893"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00334-1"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2000131"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(01)00302-4"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-75018-3_49"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2019.8702440"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00173-4"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_1"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jisa.2021.102926"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0467-0"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_26"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS51672.2020.00012"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"\u00c9tienne Andr\u00e9 Didier Lime Dylan Marinho and Jun Sun. 2022. Guaranteeing timed opacity using parametric timed model checking. ACM Transactions on Software Engineering and Methodology.","DOI":"10.1145\/3502851"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00151-3_3"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2021-2066"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79379-1_3"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10512-3_2"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2896386"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63406-3_1"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0269-9"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/2371116.2371118"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/2370741.2370744"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00215-8"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.11.044"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/11561163_8"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055875"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1080\/00207179.2014.944356"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.4304\/jcp.4.5.366-377"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/501978.501979"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2013.501"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3023872"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/1242572.1242656"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0074-0"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-008-0058-x"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijcip.2012.08.002"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77649"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2011.2166794"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/234313.234418"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.microrel.2006.07.072"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02617-1_3"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_9"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.12.002"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/1029133.1029137"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.5555\/1370677.1370679"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.4236\/ijcns.2010.310104"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0361-y"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/2808783.2808787"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/3214292.3214294"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.25596\/jalc-2001-003"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(82)90004-9"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/352600.352606"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00329-9"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2000.856935"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/2518102"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-44878-7_3"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.05.046"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1109\/NESEA.2012.6474023"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94496-8_3"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964017"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1007\/11560326_17"},{"key":"e_1_3_2_80_2","volume-title":"NWPT","author":"Godskesen Jens Chr","year":"2006","unstructured":"Jens Chr Godskesen and Olena Gryn. 2006. Modelling and verification of security protocols for ad hoc networks using UPPAAL. In NWPT. Reykjav\u00edk University."},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75454-1_15"},{"key":"e_1_3_2_82_2","volume-title":"Formal Design of Reliable Real Time Systems","author":"Gregersen H.","year":"1995","unstructured":"H. Gregersen and H. E. Jensen. 1995. Formal Design of Reliable Real Time Systems. Master\u2019s Thesis. Department of Mathematics and Computer Science, Aalborg University."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-74860-3_5"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00450-014-0257-9"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2006.1639422"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49635-0_9"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/1592451.1592452"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00037-1"},{"key":"e_1_3_2_90_2","volume-title":"ICONS","author":"Hyla Tomasz","year":"2014","unstructured":"Tomasz Hyla, Jerzy Peja\u015b, Imed El Fray, Witold Ma\u0107k\u00f3w, W\u0142odzimierz Chocianowicz, and Marcin Szulga. 2014. Sensitive information protection on mobile devices using general access structures. In ICONS. IARA."},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.5555\/2367396.2367405"},{"key":"e_1_3_2_92_2","first-page":"100","volume-title":"CS&P","author":"Jakubowska Gizela","year":"2005","unstructured":"Gizela Jakubowska, Wojciech Penczek, and Marian Srebrny. 2005. Verifying security protocols with timestamps via translation to timed automata. In CS&P, L. Czaja (Ed.). Warsaw University Press, 100\u2013115."},{"key":"e_1_3_2_93_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.11936"},{"key":"e_1_3_2_94_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46598-2_10"},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2005.1"},{"issue":"1","key":"e_1_3_2_96_2","first-page":"313","article-title":"VerICS 2007\u2014A model checker for knowledge and real-time","volume":"85","author":"Kacprzak Magdalena","year":"2008","unstructured":"Magdalena Kacprzak, Wojciech Nabialek, Artur Niewiadomski, Wojciech Penczek, Agata P\u00f3lrola, Maciej Szreter, Bozena Wozna, and Andrzej Zbrzezny. 2008. VerICS 2007\u2014A model checker for knowledge and real-time. Fundam. Inf. 85, 1-4 (2008), 313\u2013328. http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi85-1-4-22.","journal-title":"Fundam. Inf."},{"key":"e_1_3_2_97_2","doi-asserted-by":"publisher","DOI":"10.1109\/MWC.2007.4396947"},{"key":"e_1_3_2_98_2","doi-asserted-by":"publisher","DOI":"10.1145\/3078809"},{"key":"e_1_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30793-5_6"},{"key":"e_1_3_2_100_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29072-5_6"},{"key":"e_1_3_2_101_2","doi-asserted-by":"publisher","DOI":"10.1145\/3399742"},{"key":"e_1_3_2_102_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_103_2","doi-asserted-by":"publisher","DOI":"10.1109\/SSIRI-C.2010.27"},{"key":"e_1_3_2_104_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19751-2_6"},{"key":"e_1_3_2_105_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs029"},{"key":"e_1_3_2_106_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2014.07.001"},{"key":"e_1_3_2_107_2","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516712"},{"key":"e_1_3_2_108_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10506-2_22"},{"key":"e_1_3_2_109_2","doi-asserted-by":"publisher","DOI":"10.5220\/0007830605700577"},{"key":"e_1_3_2_110_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22975-1_11"},{"key":"e_1_3_2_111_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89363-1_4"},{"key":"e_1_3_2_112_2","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2017.12"},{"key":"e_1_3_2_113_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46586-9_6"},{"key":"e_1_3_2_114_2","doi-asserted-by":"publisher","DOI":"10.5555\/2367396.2367411"},{"key":"e_1_3_2_115_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2009-0100"},{"key":"e_1_3_2_116_2","doi-asserted-by":"publisher","DOI":"10.1201\/b13055-12"},{"key":"e_1_3_2_117_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"e_1_3_2_118_2","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7352"},{"key":"e_1_3_2_119_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2003.1236205"},{"key":"e_1_3_2_120_2","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-24098-5_2"},{"key":"e_1_3_2_121_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.4"},{"key":"e_1_3_2_122_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60246-1_158"},{"key":"e_1_3_2_123_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_3_2_124_2","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.34"},{"key":"e_1_3_2_125_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_31"},{"key":"e_1_3_2_126_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2712621"},{"key":"e_1_3_2_127_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2011.19"},{"key":"e_1_3_2_128_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67220-1_3"},{"key":"e_1_3_2_129_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00144-2"},{"issue":"3","key":"e_1_3_2_130_2","first-page":"93","article-title":"Breaking and fixing the needham-schroeder public-key protocol using FDR","volume":"17","author":"Lowe Gavin","year":"1996","unstructured":"Gavin Lowe. 1996. Breaking and fixing the needham-schroeder public-key protocol using FDR. Softw. Concepts Tools 17, 3 (1996), 93\u2013102.","journal-title":"Softw. Concepts Tools"},{"key":"e_1_3_2_131_2","doi-asserted-by":"publisher","DOI":"10.1142\/S021819401840020X"},{"key":"e_1_3_2_132_2","first-page":"165","volume-title":"WITS","author":"Mazar\u00e9 Laurent","year":"2004","unstructured":"Laurent Mazar\u00e9. 2004. Using unification for opacity properties. In WITS, Peter Ryan (Ed.). 165\u2013176."},{"key":"e_1_3_2_133_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIE.2005.855692"},{"key":"e_1_3_2_134_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jnca.2012.05.003"},{"key":"e_1_3_2_135_2","doi-asserted-by":"publisher","DOI":"10.1109\/IAS.2008.10"},{"key":"e_1_3_2_136_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2010.09.002"},{"key":"e_1_3_2_137_2","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_3_2_138_2","doi-asserted-by":"publisher","DOI":"10.1145\/155848.155852"},{"key":"e_1_3_2_139_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0094-1"},{"key":"e_1_3_2_140_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63121-9_1"},{"key":"e_1_3_2_141_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_33"},{"key":"e_1_3_2_142_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cag.2005.10.004"},{"key":"e_1_3_2_143_2","doi-asserted-by":"publisher","DOI":"10.17487\/RFC6275"},{"key":"e_1_3_2_144_2","volume-title":"NDSS","author":"Perrig Adrian","year":"2001","unstructured":"Adrian Perrig, Ran Canetti, Dawn Xiaodong Song, and J. D. Tygar. 2001. Efficient and secure source authentication for multicast. In NDSS. The Internet Society."},{"key":"e_1_3_2_145_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016598314198"},{"key":"e_1_3_2_146_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2019.00015"},{"key":"e_1_3_2_147_2","doi-asserted-by":"publisher","DOI":"10.1515\/amcs-2015-0031"},{"key":"e_1_3_2_148_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39426-8_13"},{"key":"e_1_3_2_149_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85735-8_6"},{"key":"e_1_3_2_150_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2015.03.001"},{"key":"e_1_3_2_151_2","doi-asserted-by":"publisher","DOI":"10.1002\/sec.1401"},{"key":"e_1_3_2_152_2","doi-asserted-by":"publisher","DOI":"10.1109\/49.1940"},{"key":"e_1_3_2_153_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.485845"},{"key":"e_1_3_2_154_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2004.842547"},{"key":"e_1_3_2_155_2","doi-asserted-by":"publisher","DOI":"10.1109\/40.977758"},{"key":"e_1_3_2_156_2","doi-asserted-by":"publisher","DOI":"10.1145\/65000.65002"},{"key":"e_1_3_2_157_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70972-7_13"},{"key":"e_1_3_2_158_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57805-3_14"},{"key":"e_1_3_2_159_2","doi-asserted-by":"publisher","DOI":"10.17512\/jamcm.2016.2.13"},{"key":"e_1_3_2_160_2","doi-asserted-by":"publisher","DOI":"10.1007\/s12927-019-0003-8"},{"key":"e_1_3_2_161_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0255(85)90026-X"},{"key":"e_1_3_2_162_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2015.06.007"},{"key":"e_1_3_2_163_2","doi-asserted-by":"publisher","DOI":"10.5220\/0010388701810188"},{"key":"e_1_3_2_164_2","doi-asserted-by":"publisher","DOI":"10.17512\/jamcm.2015.3.14"},{"key":"e_1_3_2_165_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46586-9_5"},{"key":"e_1_3_2_166_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99981-4_3"},{"key":"e_1_3_2_167_2","doi-asserted-by":"publisher","DOI":"10.3390\/s21093055"},{"key":"e_1_3_2_168_2","unstructured":"Niklas S\u00f6rensson and Niklas Een. 2005. Minisat v1.13-a SAT solver with conflict-clause minimization. In SAT Competition 2005 ."},{"key":"e_1_3_2_169_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32122-1"},{"key":"e_1_3_2_170_2","doi-asserted-by":"publisher","DOI":"10.1145\/1454630.1454638"},{"key":"e_1_3_2_171_2","doi-asserted-by":"publisher","DOI":"10.1109\/CCNC46108.2020.9045724"},{"key":"e_1_3_2_172_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TIME.2017.21"},{"key":"e_1_3_2_173_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_2"},{"key":"e_1_3_2_174_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00010"},{"key":"e_1_3_2_175_2","volume-title":"Fault Tree Handbook","author":"Vesely William E.","year":"1981","unstructured":"William E. Vesely, Francine F. Goldberg, Norman H. Roberts, and David F. Haasl. 1981. Fault Tree Handbook. Technical Report. Nuclear Regulatory Commission Washington DC."},{"key":"e_1_3_2_176_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2013.05.001"},{"key":"e_1_3_2_177_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01461-2_3"},{"key":"e_1_3_2_178_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2857363"},{"key":"e_1_3_2_179_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSC.2017.44"},{"key":"e_1_3_2_180_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_21"},{"key":"e_1_3_2_181_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2359893"},{"key":"e_1_3_2_182_2","doi-asserted-by":"publisher","DOI":"10.1145\/3331524"},{"key":"e_1_3_2_183_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29662-9_14"},{"key":"e_1_3_2_184_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57628-8_4"},{"key":"e_1_3_2_185_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_4"},{"key":"e_1_3_2_186_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_24"},{"key":"e_1_3_2_187_2","doi-asserted-by":"publisher","DOI":"10.1145\/182110.182113"},{"key":"e_1_3_2_188_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-015-9637-9"},{"key":"e_1_3_2_189_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1527"},{"key":"e_1_3_2_190_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0951-8320(01)00101-6"},{"key":"e_1_3_2_191_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"},{"key":"e_1_3_2_192_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20005-3_3"},{"key":"e_1_3_2_193_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60840-2_35"},{"key":"e_1_3_2_194_2","first-page":"2123","volume-title":"AAMAS","author":"Zbrzezny Agnieszka M.","year":"2020","unstructured":"Agnieszka M. Zbrzezny, Andrzej Zbrzezny, Sabina Szymoniak, Olga Siedlecka-Lamch, and Miros\u0142aw Kurkowski. 2020. VerSecTis\u2014An agent based model checker for security protocols. In AAMAS, Amal El Fallah Seghrouchni, Gita Sukthankar, Bo An, and Neil Yorke-Smith (Eds.). International Foundation for Autonomous Agents and Multiagent Systems, 2123\u20132125."},{"key":"e_1_3_2_195_2","doi-asserted-by":"publisher","DOI":"10.1109\/CCNC.2018.8319187"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3534967","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3534967","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:02:54Z","timestamp":1750172574000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3534967"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,7]]},"references-count":194,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,7,31]]}},"alternative-id":["10.1145\/3534967"],"URL":"https:\/\/doi.org\/10.1145\/3534967","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12,7]]},"assertion":[{"value":"2021-08-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-05-02","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-12-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}