{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T13:22:37Z","timestamp":1743081757413,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":32,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819606160"},{"type":"electronic","value":"9789819606177"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-981-96-0617-7_19","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T14:47:16Z","timestamp":1732805236000},"page":"332-352","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficient SMT-Based Model Checking for\u00a0HyperTWTL"],"prefix":"10.1007","author":[{"given":"Ernest","family":"Bonnah","sequence":"first","affiliation":[]},{"given":"Luan Viet","family":"Nguyen","sequence":"additional","affiliation":[]},{"given":"Khaza Anuarul","family":"Hoque","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Alpern, B., et al.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"19_CR2","unstructured":"ANYbotics. Automation & Digitalization at Scale: ANYmal Makes the Case at BASF (2021). https:\/\/www.anybotics.com\/anymal-makes-the-case-at-basf-chemical-plant\/"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.: Z3 and SMT in industrial R &D. In: FM, pp. 675\u2013678. Springer (2018)","DOI":"10.1007\/978-3-319-95582-7_44"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., et al.: The complexity of monitoring hyperproperties. In: 2018 IEEE 31st CSF, pp. 162\u2013174. IEEE (2018)","DOI":"10.1109\/CSF.2018.00019"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., et al.: Monitoring hyperproperties by combining static analysis and runtime verification. In: ISoLA, pp. 8\u201327. Springer (2018)","DOI":"10.1007\/978-3-030-03421-4_2"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., et al.: Controller synthesis for hyperproperties. In: 2020 IEEE 33rd CSF, pp. 366\u2013379. IEEE (2020)","DOI":"10.1109\/CSF49147.2020.00033"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., et al.: Model checking timed hyperproperties in discrete-time systems. In: NASA Formal Methods Symposium, pp. 311\u2013328. Springer (2020)","DOI":"10.1007\/978-3-030-55754-6_18"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Bonnah, E., et al.: Model checking time window temporal logic for hyperproperties. In: 21st ACM-IEEE MEMOCODE, pp. 100\u2013110 (2023)","DOI":"10.1145\/3610579.3611077"},{"key":"19_CR10","unstructured":"Clarke, E., et al.: Bounded model checking using satisfiability solving. FM 19(1), 7\u201334 (2001)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M.: Model checking. In: FSTTCS, pp. 54\u201356. Springer (1997)","DOI":"10.1007\/BFb0058022"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., et al.: Temporal logics for hyperproperties. In: POST, pp. 265\u2013284. Springer (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"19_CR13","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Coenen, N., et al.: Verifying hyperliveness. In: CAV, pp. 121\u2013139. Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., et al.: Algorithms for model checking hyperltl and hyperctl. In: CAV, pp. 30\u201348. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., et al.: Specifying and verifying secrecy in workflows with arbitrarily many agents. In: ATVA, pp. 157\u2013173. Springer (2016)","DOI":"10.1007\/978-3-319-46520-3_11"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., et al.: Model checking quantitative hyperproperties. In: CAV, pp. 144\u2013163. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B.E.A.: Eahyper: satisfiability, implication, and equivalence checking of hyperproperties. In: CAV, pp. 564\u2013570. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_29"},{"key":"19_CR19","unstructured":"Garey, M.R., et al.: Computers and Intractability. A Guide to the (1979)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., et al.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, pp. 11\u201311. IEEE (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"19_CR21","unstructured":"Ho, H.M., et. al: On verifying timed hyperproperties. arXiv preprint arXiv:1812.10005 (2018)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Hsu, T.H., et al.: Hyperqube: a QBF-based bounded model checker for hyperproperties. arXiv preprint arXiv:2109.12989 (2021)","DOI":"10.26226\/morressier.604907f41a80aac83ca25cec"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Hsu, T.H., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: TACAS, pp. 94\u2013112. Springer (2021)","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"19_CR24","unstructured":"Knightscope. Knightscope Deploys New Autonomous Security Robot in Southern California (2022). https:\/\/www.businesswire.com\/news\/home\/20220316005436\/en\/Knightscope-Deploys-New-Autonomous-Security-Robot-in-Southern-California"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Nguyen, L.V., et al.: Hyperproperties of real-valued signals. In: MEMOCODE, pp. 104\u2013113 (2017)","DOI":"10.1145\/3127041.3127058"},{"key":"19_CR26","unstructured":"Paviot-Adet, E., et al.: Structural reductions and stutter sensitive properties. arXiv preprint arXiv:2212.04218 (2022)"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Pommellet, A., et al.: Model-checking hyperltl for pushdown systems. In: SPIN, pp. 133\u2013152. Springer (2018)","DOI":"10.1007\/978-3-319-94111-0_8"},{"key":"19_CR28","unstructured":"Romano, S.A.: Persistent surveillance gives squadron its global purpose. https:\/\/www.af.mil\/News\/Article-Display\/Article\/1152329\/persistent-surveillance-gives-squadron-its-global-purpose\/"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Rungta, N.: A billion SMT queries a day. In: CAV, pp. 3\u201318. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Vasile, C.I., et al.: Time window temporal logic. Theoret. Comput. Sci. 691, 27\u201354 (2017)","DOI":"10.1016\/j.tcs.2017.07.012"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Wang, Y., et al.: Hyperproperties for robotics: planning via hyperltl. In: 2020 IEEE ICRA, pp. 8462\u20138468. IEEE (2020)","DOI":"10.1109\/ICRA40945.2020.9196874"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., et al.: Observational determinism for concurrent program security. In: 16th IEEE CSF, pp. 29\u201343. IEEE (2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0617-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T15:09:51Z","timestamp":1732806591000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0617-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9789819606160","9789819606177"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0617-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hiroshima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.icfem2024.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}