{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T08:11:50Z","timestamp":1790842310883,"version":"4.1.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. VLDB Endow."],"published-print":{"date-parts":[[2017,11]]},"abstract":"<jats:p>Data-driven workflows, of which IBM's Business Artifacts are a prime exponent, have been successfully deployed in practice, adopted in industrial standards, and have spawned a rich body of research in academia, focused primarily on static analysis. The present research bridges the gap between the theory and practice of artifact verification with VERIFAS, the first implementation of practical significance of an artifact verifier with full support for unbounded data. VERIFAS verifies within seconds linear-time temporal properties over real-world and synthetic workflows of complexity in the range recommended by software engineering practice. Compared to our previous implementation based on the widely-used Spin model checker, VERIFAS not only supports a model with richer data manipulations but also outperforms it by over an order of magnitude. VERIFAS' good performance is due to a novel symbolic representation approach and a family of specialized optimizations.<\/jats:p>","DOI":"10.14778\/3157794.3157798","type":"journal-article","created":{"date-parts":[[2017,12,12]],"date-time":"2017-12-12T18:33:38Z","timestamp":1513103618000},"page":"283-296","source":"Crossref","is-referenced-by-count":20,"title":["VERIFAS"],"prefix":"10.14778","volume":"11","author":[{"given":"Yuliang","family":"Li","sequence":"first","affiliation":[{"name":"UC San Diego"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alin","family":"Deutsch","sequence":"additional","affiliation":[{"name":"UC San Diego"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor","family":"Vianu","sequence":"additional","affiliation":[{"name":"UC San Diego &amp; INRIA Paris"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,11]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"MIST - a safety checker for Petri nets and extensions. https:\/\/github.com\/pierreganty\/mist\/wiki. Accessed: 2017-04-13.  MIST - a safety checker for Petri nets and extensions. https:\/\/github.com\/pierreganty\/mist\/wiki. Accessed: 2017-04-13."},{"key":"e_1_2_1_2_1","unstructured":"Object management group business process model and notation. http:\/\/www.bpmn.org\/. Accessed: 2017-03-01.  Object management group business process model and notation. http:\/\/www.bpmn.org\/. Accessed: 2017-03-01."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2902251.2902300"},{"key":"e_1_2_1_4_1","volume-title":"Petri Nets","author":"Badouel E.","year":"2015","unstructured":"E. Badouel , L. H\u00e9lou\u00ebt , and C. Morvan . Petri nets with semi-structured data . In Petri Nets , 2015 . E. Badouel, L. H\u00e9lou\u00ebt, and C. Morvan. Petri nets with semi-structured data. In Petri Nets, 2015."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34321-6_2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.464.0703"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.441.0145"},{"key":"e_1_2_1_8_1","first-page":"108","volume-title":"Mathematical Foundations of Computer Science","author":"Blockelet M.","year":"2011","unstructured":"M. Blockelet and S. Schmitz . Model checking coverability graphs of vector addition systems . In Mathematical Foundations of Computer Science 2011 , pages 108 -- 119 . Springer , 2011. M. Blockelet and S. Schmitz. Model checking coverability graphs of vector addition systems. In Mathematical Foundations of Computer Science 2011, pages 108--119. Springer, 2011."},{"key":"e_1_2_1_9_1","first-page":"2031","volume-title":"AAAI","author":"Calvanese D.","year":"2015","unstructured":"D. Calvanese , G. Delzanno , and M. Montali . Verification of relational multiagent systems with data types . In AAAI , pages 2031 -- 2037 , 2015 . D. Calvanese, G. Delzanno, and M. Montali. Verification of relational multiagent systems with data types. In AAAI, pages 2031--2037, 2015."},{"key":"e_1_2_1_10_1","volume-title":"BPM","author":"Chao T.","year":"2009","unstructured":"T. Chao Artifact-based transformation of IBM Global Financing: A case study . In BPM , 2009 . T. Chao et al. Artifact-based transformation of IBM Global Financing: A case study. In BPM, 2009."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338626.2338628"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2012.09.002"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218843012500025"},{"key":"e_1_2_1_14_1","volume-title":"Case management: Cordys approach. BP Trends (www.bptrends.com)","author":"de Man H.","year":"2009","unstructured":"H. de Man . Case management: Cordys approach. BP Trends (www.bptrends.com) , 2009 . H. de Man. Case management: Cordys approach. BP Trends (www.bptrends.com), 2009."},{"key":"e_1_2_1_15_1","volume-title":"AAAI","author":"De Masellis R.","year":"2017","unstructured":"R. De Masellis , C. Di Francescomarino , C. Ghidini , M. Montali , and S. Tessaris . Add data into business process verification: Bridging the gap between theory and practice . In AAAI , 2017 . R. De Masellis, C. Di Francescomarino, C. Ghidini, M. Montali, and S. Tessaris. Add data into business process verification: Bridging the gap between theory and practice. In AAAI, 2017."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514924"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2902251.2902275"},{"key":"e_1_2_1_18_1","volume-title":"VERIFAS: A practical verifier for artifact systems (extended version). arXiv preprint, arXiv:1705.10007","author":"Deutsch A.","year":"2017","unstructured":"A. Deutsch , Y. Li , and V. Vianu . VERIFAS: A practical verifier for artifact systems (extended version). arXiv preprint, arXiv:1705.10007 , 2017 . A. Deutsch, Y. Li, and V. Vianu. VERIFAS: A practical verifier for artifact systems (extended version). arXiv preprint, arXiv:1705.10007, 2017."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066157.1066219"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142473.1142584"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56689-9_45"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054110007180"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICWS.2012.31"},{"key":"e_1_2_1_24_1","first-page":"54","volume-title":"ICSOC","author":"Gonzalez P.","year":"2013","unstructured":"P. Gonzalez , A. Griesmayer , and A. Lomuscio . Model checking gsm-based multi-agent systems . In ICSOC , pages 54 -- 68 , 2013 . P. Gonzalez, A. Griesmayer, and A. Lomuscio. Model checking gsm-based multi-agent systems. In ICSOC, pages 54--68, 2013."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48616-0_16"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2465221"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1405716"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2002259.2002270"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/800152.804905"},{"key":"e_1_2_1_30_1","volume-title":"The data warehouse toolkit: the complete guide to dimensional modeling","author":"Kimball R.","year":"2011","unstructured":"R. Kimball and M. Ross . The data warehouse toolkit: the complete guide to dimensional modeling . John Wiley & Sons , 2011 . R. Kimball and M. Ross. The data warehouse toolkit: the complete guide to dimensional modeling. John Wiley & Sons, 2011."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1497079.1497082"},{"key":"e_1_2_1_32_1","volume-title":"A Spin-based verifier for artifact systems. arXiv preprint, arXiv:1705.09427","author":"Li Y.","year":"2017","unstructured":"Y. Li , A. Deutsch , and V. Vianu . A Spin-based verifier for artifact systems. arXiv preprint, arXiv:1705.09427 , 2017 . Y. Li, A. Deutsch, and V. Vianu. A Spin-based verifier for artifact systems. arXiv preprint, arXiv:1705.09427, 2017."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1394399"},{"key":"e_1_2_1_34_1","volume-title":"BPM Workshops","author":"Marin M.","year":"2012","unstructured":"M. Marin , R. Hull , and R. Vacul\u00edn . Data centric bpm and the emerging case management standard: A short survey . In BPM Workshops , 2012 . M. Marin, R. Hull, and R. Vacul\u00edn. Data centric bpm and the emerging case management standard: A short survey. In BPM Workshops, 2012."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.423.0428"},{"key":"e_1_2_1_36_1","volume-title":"Case Management Model and Notation (CMMN)","author":"Object Management Group","year":"2014","unstructured":"Object Management Group . Case Management Model and Notation (CMMN) , 2014 . Object Management Group. Case Management Model and Notation (CMMN), 2014."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/2022192.2022199"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205003"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.007"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2011.04.004"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211865"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_2_1_44_1","volume-title":"SIAM journal on computing, 1(2):146--160","author":"Tarjan R.","year":"1972","unstructured":"R. Tarjan . Depth-first search and linear graph algorithms. SIAM journal on computing, 1(2):146--160 , 1972 . R. Tarjan. Depth-first search and linear graph algorithms. SIAM journal on computing, 1(2):146--160, 1972."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1155\/2013\/507984"},{"key":"e_1_2_1_46_1","volume-title":"LICS","author":"Vardi M. Y.","year":"1986","unstructured":"M. Y. Vardi and P. Wolper . An automata-theoretic approach to automatic program verification . In LICS , 1986 . M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS, 1986."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/344816.344869"},{"key":"e_1_2_1_48_1","volume-title":"Structured testing: A testing methodology using the cyclomatic complexity metric","author":"Watson A. H.","year":"1996","unstructured":"A. H. Watson , D. R. Wallace , and T. J. McCabe . Structured testing: A testing methodology using the cyclomatic complexity metric , volume 500 . US Department of Commerce, Technology Administration , National Institute of Standards and Technology , 1996 . A. H. Watson, D. R. Wallace, and T. J. McCabe. Structured testing: A testing methodology using the cyclomatic complexity metric, volume 500. US Department of Commerce, Technology Administration, National Institute of Standards and Technology, 1996."},{"key":"e_1_2_1_49_1","volume-title":"IBM Redbooks","author":"Zhu W.-D.","year":"2015","unstructured":"W.-D. Zhu Advanced Case Management with IBM Case Manager . IBM Redbooks , 2015 . W.-D. Zhu et al. Advanced Case Management with IBM Case Manager. IBM Redbooks, 2015."}],"container-title":["Proceedings of the VLDB Endowment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.14778\/3157794.3157798","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T09:36:53Z","timestamp":1672220213000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.14778\/3157794.3157798"}},"subtitle":["a practical verifier for artifact systems"],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["10.14778\/3157794.3157798"],"URL":"https:\/\/doi.org\/10.14778\/3157794.3157798","relation":{},"ISSN":["2150-8097"],"issn-type":[{"value":"2150-8097","type":"print"}],"subject":[],"published":{"date-parts":[[2017,11]]}}}