{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T18:30:32Z","timestamp":1791484232540,"version":"4.3.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030266189","type":"print"},{"value":"9783030266196","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-26619-6_12","type":"book-chapter","created":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T19:12:33Z","timestamp":1566501153000},"page":"157-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN"],"prefix":"10.1007","author":[{"given":"Diego","family":"Calvanese","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Gianola","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"Montali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Rivkin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,7,23]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Calvanese, D., De Giacomo, G., Montali, M.: Foundations of data aware process analysis: a database theory perspective. In: Proceedings of the PODS, pp. 1\u201312 (2013)","DOI":"10.1145\/2463664.2467796"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal modeling and SMT-based parameterized verification of data-aware BPMN (extended version). Technical report arXiv:1906.07811 (2019)","DOI":"10.1007\/978-3-030-26619-6_12"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal modeling and SMT-based parameterized verification of multi-case data-aware BPMN. Technical report arXiv:1905.12991 (2019)","DOI":"10.1007\/978-3-030-26619-6_12"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-030-22102-7_10","volume-title":"Description Logic, Theory Combination, and All That","author":"D Calvanese","year":"2019","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: From model completeness to verification of data aware processes. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.Y., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 212\u2013239. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22102-7_10"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Automated Deduction - CADE 27, LNCS (LNAI), vol. 11716. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-29436-6_9"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-030-00847-5_18","volume-title":"Conceptual Modeling","author":"C Combi","year":"2018","unstructured":"Combi, C., Oliboni, B., Weske, M., Zerbato, F.: Conceptual modeling of processes and data: connecting different perspectives. In: Trujillo, J., et al. (eds.) ER 2018. LNCS, vol. 11157, pp. 236\u2013250. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00847-5_18"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1007\/978-3-319-59536-8_38","volume-title":"Advanced Information Systems Engineering","author":"G De Giacomo","year":"2017","unstructured":"De Giacomo, G., Oriol, X., Esta\u00f1ol, M., Teniente, E.: Linking data and BPMN processes to achieve executable models. In: Dubois, E., Pohl, K. (eds.) CAiSE 2017. LNCS, vol. 10253, pp. 612\u2013628. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59536-8_38"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-030-00847-5_17","volume-title":"Conceptual Modeling","author":"M de Leoni","year":"2018","unstructured":"de Leoni, M., Felli, P., Montali, M.: A holistic approach for soundness verification of decision-aware process models. In: Trujillo, J., et al. (eds.) ER 2018. LNCS, vol. 11157, pp. 219\u2013235. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00847-5_17"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"De Masellis, R., Di Francescomarino, C., Ghidini, C., Montali, M., Tessaris, S.: Add data into business process verification: bridging the gap between theory and practice. In: Proceedings of AAAI, pp. 1091\u20131099. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.10688"},{"issue":"2","key":"12_CR10","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/3212019.3212025","volume":"5","author":"A Deutsch","year":"2018","unstructured":"Deutsch, A., Hull, R., Li, Y., Vianu, V.: Automatic verification of database-centric systems. SIGLOG News 5(2), 37\u201356 (2018)","journal-title":"SIGLOG News"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Li, Y., Vianu, V.: Verification of hierarchical artifact systems. In: Proceedings of the PODS, pp. 179\u2013194 (2016)","DOI":"10.1145\/2902251.2902275"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-319-19069-3_27","volume-title":"Advanced Information Systems Engineering","author":"M Esta\u00f1ol","year":"2015","unstructured":"Esta\u00f1ol, M., Sancho, M.-R., Teniente, E.: Verification and validation of UML artifact-centric business process models. In: Zdravkovic, J., Kirikova, M., Johannesson, P. (eds.) CAiSE 2015. LNCS, vol. 9097, pp. 434\u2013449. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19069-3_27"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-71070-7_6","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67\u201382. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_6"},{"issue":"4","key":"12_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-6(4:10)2010","volume":"6","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4), 1\u201348 (2010)","journal-title":"Log. Methods Comput. Sci."},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22\u201329. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_3"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-39086-4_3","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"S Lasota","year":"2016","unstructured":"Lasota, S.: Decidability border for Petri nets with data: WQO dichotomy conjecture. In: Kordon, F., Moldt, D. (eds.) PETRI NETS 2016. LNCS, vol. 9698, pp. 20\u201336. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39086-4_3"},{"issue":"3","key":"12_CR17","first-page":"283","volume":"11","author":"Y Li","year":"2017","unstructured":"Li, Y., Deutsch, A., Vianu, V.: VERIFAS: a practical verifier for artifact systems. PVLDB 11(3), 283\u2013296 (2017)","journal-title":"PVLDB"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-40176-3_14","volume-title":"Business Process Management","author":"A Meyer","year":"2013","unstructured":"Meyer, A., Pufahl, L., Fahland, D., Weske, M.: Modeling and enacting complex data dependencies in business processes. In: Daniel, F., Wang, J., Weber, B. (eds.) BPM 2013. LNCS, vol. 8094, pp. 171\u2013186. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40176-3_14"},{"issue":"4","key":"12_CR19","first-page":"91","volume":"28","author":"M Montali","year":"2017","unstructured":"Montali, M., Rivkin, A.: DB-Nets: on the marriage of colored Petri Nets and relational databases. ToPNoC 28(4), 91\u2013118 (2017)","journal-title":"ToPNoC"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-540-76848-7_10","volume-title":"On the Move to Meaningful Internet Systems 2007: CoopIS, DOA, ODBASE, GADA, and IS","author":"D M\u00fcller","year":"2007","unstructured":"M\u00fcller, D., Reichert, M., Herbst, J.: Data-driven modeling and coordination of large process structures. In: Meersman, R., Tari, Z. (eds.) OTM 2007. LNCS, vol. 4803, pp. 131\u2013149. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76848-7_10"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-33606-5_2","volume-title":"On the Move to Meaningful Internet Systems: OTM 2012","author":"M Reichert","year":"2012","unstructured":"Reichert, M.: Process and data: two sides of the same coin? In: Meersman, R., et al. (eds.) OTM 2012. LNCS, vol. 7565, pp. 2\u201319. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33606-5_2"},{"issue":"34","key":"12_CR22","doi-asserted-by":"publisher","first-page":"4439","DOI":"10.1016\/j.tcs.2011.05.007","volume":"412","author":"F Rosa-Velardo","year":"2011","unstructured":"Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci. 412(34), 4439\u20134451 (2011)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"12_CR23","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1016\/j.is.2011.04.004","volume":"36","author":"N Sidorova","year":"2011","unstructured":"Sidorova, N., Stahl, C., Trcka, N.: Soundness verification for conceptual workflow nets with data: early detection of errors with the most precision possible. Inf. Syst. 36(7), 1026\u20131043 (2011)","journal-title":"Inf. Syst."},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-63139-9_48","volume-title":"Application and Theory of Petri Nets 1997","author":"WMP Aalst","year":"1997","unstructured":"Aalst, W.M.P.: Verification of workflow nets. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 407\u2013426. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63139-9_48"}],"container-title":["Lecture Notes in Computer Science","Business Process Management"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-26619-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,23]],"date-time":"2024-08-23T14:16:54Z","timestamp":1724422614000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-26619-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030266189","9783030266196"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-26619-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"BPM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Business Process Management","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vienna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"bpm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/bpm2019.ai.wu.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":"115","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":"23","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":"4","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":"20% - 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":"5","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"In addition, 13 papers were published from the BPM forum","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)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}