{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,28]],"date-time":"2025-06-28T11:26:30Z","timestamp":1751109990194,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030605070"},{"type":"electronic","value":"9783030605087"}],"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"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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-60508-7_6","type":"book-chapter","created":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T04:33:06Z","timestamp":1602045186000},"page":"107-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["BDDs for Representing Data in Runtime Verification"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,2]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Alfaro","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395\u2013410. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_27"},{"issue":"3","key":"6_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"issue":"2\/3","key":"6_CR3","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"RI Bahar","year":"1997","unstructured":"Bahar, R.I., et al.: Algebraic decision diagrams and their applications. Formal Methods Syst. Des. 10(2\/3), 171\u2013206 (1997)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"6_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 1\u201345 (2015)","journal-title":"J. ACM"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/11678779_15","volume-title":"Hardware and Software, Verification and Testing","author":"S Bensalem","year":"2006","unstructured":"Bensalem, S., Havelund, K.: Dynamic deadlock analysis of multi-threaded programs. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 208\u2013223. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11678779_15"},{"issue":"8","key":"6_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"6_CR7","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"6_CR8","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"RE Bryant","year":"1991","unstructured":"Bryant, R.E.: On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205\u2013213 (1991)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR9","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond, pp. 428\u2013439, LICS (1990)"},{"key":"6_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)"},{"issue":"2\/3","key":"6_CR11","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1023\/A:1008695706493","volume":"10","author":"EM Clarke","year":"1997","unstructured":"Clarke, E.M., McMillan, K.L., Zhao, X.G., Fujita, M., Yang, J.C.-Y.: Spectral transforms for large boolean functions with applications to technology mapping. Formal Methods Syst. Des. 10(2\/3), 137\u2013148 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the Temporal Basis of Fairness, POPL, pp. 163\u2013173. ACM Press (1980)","DOI":"10.1145\/567446.567462"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-03427-6_8","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"K Havelund","year":"2018","unstructured":"Havelund, K., Peled, D.: BDDs on the run. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 58\u201369. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_8"},{"key":"6_CR14","unstructured":"Havelund, K., Peled, D.: First-order timed runtime verification using BDDs. In: ATVA. LNCS. Springer (to appear, 2020)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. In: FMCAD, pp. 116\u2013123. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. Formal Methods Syst. Des. 1\u201321 (2019). https:\/\/doi.org\/10.1007\/s10703-018-00327-4","DOI":"10.1007\/s10703-018-00327-4"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-75632-5_3","volume-title":"Lectures on Runtime Verification","author":"K Havelund","year":"2018","unstructured":"Havelund, K., Reger, G., Thoma, D., Z\u0103linescu, E.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 61\u2013102. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"6_CR19","unstructured":"JavaBDD. http:\/\/javabdd.sourceforge.net"},{"issue":"3","key":"6_CR20","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR21","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"CY Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 985\u2013999 (1959)","journal-title":"Bell Syst. Tech. J."},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83, 91\u2013130 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Minato, S.: Zero-Suppressed BDDs for set manipulation in combinatorial problems. In: Design Automation Conference, pp. 272\u2013277. ACM\/IEEE (1993)","DOI":"10.1145\/157485.164890"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-60508-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T12:53:07Z","timestamp":1619268787000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-60508-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030605070","9783030605087"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-60508-7_6","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":"2 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","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":"6 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv20.ait.ac.at\/","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":"43","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":"14","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":"2","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":"33% - 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.95","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":"3.82","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)"}},{"value":"Also accepted and included: an invited paper, 5 tutorial, 6 tool papers, and a benchmark paper. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}