{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:31:11Z","timestamp":1743129071059,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030393212"},{"type":"electronic","value":"9783030393229"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-39322-9_11","type":"book-chapter","created":{"date-parts":[[2020,1,14]],"date-time":"2020-01-14T19:03:59Z","timestamp":1579028639000},"page":"226-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Systematic Classification of Attackers via Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Eric","family":"Rothstein-Morris","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Sudipta","family":"Chattopadhyay","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,1,13]]},"reference":[{"key":"11_CR1","unstructured":"November 2011. http:\/\/fmv.jku.at\/hwmcc11\/index.html"},{"key":"11_CR2","unstructured":"October 2013. http:\/\/fmv.jku.at\/hwmcc13\/index.html"},{"key":"11_CR3","unstructured":"September 2019. http:\/\/fmv.jku.at\/cadical\/"},{"key":"11_CR4","unstructured":"November 2020. https:\/\/gitlab.com\/asset-sutd\/public\/aig-ac"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-27813-9_8","volume-title":"Computer Aided Verification","author":"M Awedh","year":"2004","unstructured":"Awedh, M., Somenzi, F.: Proving more properties with bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 96\u2013108. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_8"},{"issue":"2","key":"11_CR6","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2658996","volume":"17","author":"D Basin","year":"2014","unstructured":"Basin, D., Cremers, C.: Know your enemy: compromising adversaries in protocol analysis. ACM Trans. Inf. Syst. Secur. 17(2), 7:1\u20137:31 (2014). https:\/\/doi.org\/10.1145\/2658996","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"11_CR7","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"issue":"5","key":"11_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-2(5:5)2006","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1\u201364 (2006)","journal-title":"Log. Methods Comput. Sci."},{"key":"11_CR10","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr, Linz, Austria (2011)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31612-8_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 1\u201314. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_1"},{"issue":"3","key":"11_CR13","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s10009-017-0451-8","volume":"20","author":"G Cabodi","year":"2018","unstructured":"Cabodi, G., et al.: To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking. Int. J. Softw. Tools Technol. Transf. 20(3), 313\u2013325 (2018). https:\/\/doi.org\/10.1007\/s10009-017-0451-8","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Nocco, S.: Optimized model checking of multiple properties. In: 2011 Design, Automation Test in Europe, pp. 1\u20134, March 2011","DOI":"10.1109\/DATE.2011.5763279"},{"issue":"4","key":"11_CR15","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1002\/spe.2321","volume":"46","author":"Gianpiero Cabodi","year":"2015","unstructured":"Cabodi, G., Camurati, P., Quer, S.: A graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties. Softw.: Pract. Exp. 46(4), 493\u2013511 (2016). https:\/\/doi.org\/10.1002\/spe.2321","journal-title":"Software: Practice and Experience"},{"key":"11_CR16","first-page":"135","volume":"9","author":"G Cabodi","year":"2015","unstructured":"Cabodi, G., et al.: Hardware model checking competition 2014: an analysis and comparison of model checkers and benchmarks. J. Satisf. Boolean Model. Comput. 9, 135\u2013172 (2015)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"C\u00e1rdenas, A.A., Amin, S., Lin, Z.S., Huang, Y.L., Huang, C.Y., Sastry, S.: Attacks against process control systems: risk assessment, detection, and response. In: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security. ASIACCS 2011, pp. 355\u2013366. ACM, New York (2011), https:\/\/doi.org\/10.1145\/1966913.1966959","DOI":"10.1145\/1966913.1966959"},{"key":"11_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","first-page":"76:1","DOI":"10.1145\/3203245","volume":"51","author":"J Giraldo","year":"2018","unstructured":"Giraldo, J., et al.: A survey of physics-based attack detection in cyber-physical systems. ACM Comput. Surv. 51(4), 76:1\u201376:36 (2018). https:\/\/doi.org\/10.1145\/3203245","journal-title":"ACM Comput. Surv."},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Goldberg, E., G\u00fcdemann, M., Kroening, D., Mukherjee, R.: Efficient verification of multi-property designs (the benefit of wrong assumptions). In: 2018 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 43\u201348, March 2018","DOI":"10.23919\/DATE.2018.8341977"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/3-540-46885-4_5","volume-title":"Advances in Cryptology \u2014 EUROCRYPT \u201989","author":"CG G\u00fcnther","year":"1990","unstructured":"G\u00fcnther, C.G.: An identity-based key-exchange protocol. In: Quisquater, J.-J., Vandewalle, J. (eds.) EUROCRYPT 1989. LNCS, vol. 434, pp. 29\u201337. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-46885-4_5"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: Actual Causality. MIT Press (2016). http:\/\/www.jstor.org\/stable\/j.ctt1f5g5p9","DOI":"10.7551\/mitpress\/10809.001.0001"},{"issue":"3","key":"11_CR23","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/PGEC.1963.263531","volume":"12","author":"L Hellerman","year":"1963","unstructured":"Hellerman, L.: A catalog of three-variable or-invert and and-invert logical circuits. IEEE Trans. Electron. Comput. EC 12(3), 198\u2013223 (1963)","journal-title":"IEEE Trans. Electron. Comput. EC"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Kroening","year":"2003","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 298\u2013309. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36384-X_24"},{"issue":"12","key":"11_CR25","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377\u20131394 (2002)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"11_CR27","volume-title":"Handbook of Applied Cryptography","author":"AJ Menezes","year":"1996","unstructured":"Menezes, A.J., Vanstone, S.A., Oorschot, P.C.V.: Handbook of Applied Cryptography, 1st edn. CRC Press Inc., Boca Raton (1996)","edition":"1"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-319-45741-3_22","volume-title":"Computer Security \u2013 ESORICS 2016","author":"M Rocchetto","year":"2016","unstructured":"Rocchetto, M., Tippenhauer, N.O.: On attacker models and profiles for cyber-physical systems. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 427\u2013449. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45741-3_22"},{"key":"11_CR29","unstructured":"Rothstein-Morris, E., Sun, J., Chattopadhyay, S.: Systematic Classification of Attackers via Bounded Model Checking (Extended Version). arXiv:1911.05808 (2019). http:\/\/arxiv.org\/abs\/1911.05808"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Rothstein, E., Murguia, C.G., Ochoa, M.: Design-time quantification of integrity in cyber-physical systems. In: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS 2017, pp. 63\u201374. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3139337.3139347","DOI":"10.1145\/3139337.3139347"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Tseitin, G. S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic (1967\u20131970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Urbina, D.I., et al.: Limiting the impact of stealthy attacks on industrial control systems. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. CCS 2016, pp. 1092\u20131105. ACM, New York (2016), https:\/\/doi.org\/10.1145\/2976749.2978388","DOI":"10.1145\/2976749.2978388"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Weerakkody, S., Sinopoli, B., Kar, S., Datta, A.: Information flow for security in control systems. In: 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 5065\u20135072, December 2016","DOI":"10.1109\/CDC.2016.7799044"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-39322-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T18:44:11Z","timestamp":1710269051000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-39322-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030393212","9783030393229"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-39322-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Orleans, LA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2020a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl20.sigplan.org\/home\/VMCAI-2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}