@article(aalepcist,
 author       = {{W.M.P. van der} Aalst},
 year         = {1999},
 title        = {{Formalization and Verification of Event-driven Process Chains}},
 journal      = {Information and Software Technology},
 volume       = {41},
 number       = {10},
 pages        = {639--650},
 doi          = {10.1016/S0950-5849(99)00016-6},
)
@inproceedings(AAAF16,
 author       = {P. A. Abdulla and C. Aiswarya and M. F. Atig and M. Montali and O. Rezine},
 year         = {2016},
 title        = {Recency-Bounded Verification of Dynamic Database-Driven Systems},
 booktitle    = {Proc.\ PODS},
 publisher    = {ACM Press},
 pages        = {195--210},
 doi          = {10.1145/2902251.2902300},
)
@inproceedings(AKMV19,
 author       = {A. Artale and A. Kovtunova and M. Montali and W. M. P. van der Aalst},
 year         = {2019},
 title        = {Modeling and Reasoning over Declarative Data-Aware Processes with Object-Centric Behavioral Constraints},
 booktitle    = {Proc.\ BPM},
 publisher    = {Springer},
 pages        = {139--156},
 doi          = {10.1007/978-3-030-26619-6\_11},
)
@article(BaLM16,
 author       = {E. Badouel and L. H{\'{e}}lou{\"{e}}t and C. Morvan},
 year         = {2016},
 title        = {Petri Nets with Structured Data},
 journal      = {Fundam. Inform.},
 volume       = {146},
 number       = {1},
 pages        = {35--82},
 doi          = {10.3233/FI-2016-1375},
)
@inproceedings(BCDDM13,
 author       = {Bagheri Hariri, B. and D. Calvanese and De Giacomo, G. and A. Deutsch and M. Montali},
 year         = {2013},
 title        = {Verification of Relational Data-centric Dynamic Systems with External Services},
 booktitle    = {Proc.\ PODS},
 pages        = {163--174},
 doi          = {10.1145/2463664.2465221},
)
@inproceedings(BeLP12,
 author       = {F. Belardinelli and A. Lomuscio and F. Patrizi},
 year         = {2012},
 title        = {An Abstraction Technique for the Verification of Artifact-Centric Systems},
 booktitle    = {Proc.\ of KR},
 url          = {http://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4531},
)
@inproceedings(boj,
 author       = {M. Boja{\'{n}}czyk and L. Segoufin and S. Toru{\'{n}}czyk},
 year         = {2013},
 title        = {Verification of database-driven systems via amalgamation},
 booktitle    = {Proc.\ of PODS},
 pages        = {63--74},
 doi          = {10.1145/2463664.2465228},
)
@inproceedings(CaDM13,
 author       = {D. Calvanese and De Giacomo, G. and M. Montali},
 year         = {2013},
 title        = {Foundations of Data Aware Process Analysis: {A} Database Theory Perspective},
 booktitle    = {Proc.\ PODS},
 pages        = {1--12},
 doi          = {10.1145/2463664.2467796},
)
@techreport(CGGMR18,
 author       = {D. Calvanese and S. Ghilardi and A. Gianola and M. Montali and A. Rivkin},
 year         = {2018},
 title        = {Verification of Data-Aware Processes via Array-Based Systems (Extended Version)},
 type         = {Technical Report},
 number       = {arXiv:1806.11459},
 institution  = {arXiv.org},
 url          = {https://arxiv.org/abs/1806.11459},
)
@inproceedings(CGGMR19-bpm,
 author       = {D. Calvanese and S. Ghilardi and A. Gianola and M. Montali and A. Rivkin},
 year         = {2019},
 title        = {Formal Modeling and {SMT}-Based Parameterized Verification of Data-Aware {BPMN}},
 booktitle    = {Proc.\ BPM},
 publisher    = {Springer},
 pages        = {157--175},
 doi          = {10.1007/978-3-030-26619-6\_12},
)
@inproceedings(CGGMR19,
 author       = {D. Calvanese and S. Ghilardi and A. Gianola and M. Montali and A. Rivkin},
 year         = {2019},
 title        = {From Model Completeness to Verification of Data Aware Processes},
 booktitle    = {Description Logic, Theory Combination, and All That},
 publisher    = {Springer},
 pages        = {212--239},
 doi          = {10.1007/978-3-030-22102-7\_10},
)
@inproceedings(CADE19,
 author       = {D. Calvanese and S. Ghilardi and A. Gianola and M. Montali and A. Rivkin},
 year         = {2019},
 title        = {Model Completeness, Covers and Superposition},
 booktitle    = {Proc.\ of {CADE}},
 pages        = {142--160},
 doi          = {10.1007/978-3-030-29436-6\_9},
)
@article(MSCS19,
 author       = {D. Calvanese and S. Ghilardi and A. Gianola and M. Montali and A. Rivkin},
 year         = {To appear},
 title        = {{SMT}-based Verification of Data-Aware Processes: a Model-Theoretic Approach},
 journal      = {Mathematical Structures in Computer Science},
)
@inproceedings(CaMS15,
 author       = {D. Calvanese and M. Montali and A. Santoso},
 year         = {2015},
 title        = {Verification of Generalized Inconsistency-Aware Knowledge and Action Bases},
 booktitle    = {Proc.\ IJCAI},
 publisher    = {AAAI Press},
 pages        = {2847--2853},
 url          = {http://ijcai.org/Abstract/15/403},
)
@article(DaDV12,
 author       = {E. Damaggio and A. Deutsch and V. Vianu},
 year         = {2012},
 title        = {Artifact Systems with Data Dependencies and Arithmetic},
 journal      = {ACM TODS},
 volume       = {37},
 number       = {3},
 pages        = {22:1--22:36},
 doi          = {10.1145/2338626.2338628},
)
@inproceedings(DeFM18,
 author       = {{de Leoni}, M. and P. Felli and M. Montali},
 year         = {2018},
 title        = {A Holistic Approach for Soundness Verification of Decision-Aware Process Models},
 booktitle    = {Proc.\ ER},
 pages        = {219--235},
 doi          = {10.1007/978-3-030-00847-5\_17},
)
@inproceedings(DDG16,
 author       = {De Masellis, R. and Di Francescomarino, C. and C. Ghidini and M. Montali and S. Tessaris},
 year         = {2017},
 title        = {Add Data into Business Process Verification: Bridging the Gap between Theory and Practice},
 booktitle    = {Proc.\ AAAI},
 publisher    = {AAAI Press},
 pages        = {1091--1099},
 url          = {http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14627},
)
@inproceedings(DHPV09,
 author       = {A. Deutsch and R. Hull and F. Patrizi and V. Vianu},
 year         = {2009},
 title        = {Automatic Verification of Data-Centric Business Processes},
 booktitle    = {Proc.\ of ICDT},
 pages        = {252--267},
 doi          = {10.1145/1514894.1514924},
)
@inproceedings(DeLV16,
 author       = {A. Deutsch and Y. Li and V. Vianu},
 year         = {2016},
 title        = {Verification of Hierarchical Artifact Systems},
 booktitle    = {Proc.\ PODS},
 publisher    = {ACM Press},
 pages        = {179--194},
 doi          = {10.1145/2902251.2902275},
)
@inproceedings(Dum11,
 author       = {M. Dumas},
 year         = {2011},
 title        = {On the Convergence of Data and Process Engineering},
 booktitle    = {Proc.\ of ADBIS},
 pages        = {19--26},
 doi          = {10.1007/978-3-642-23737-9\_2},
)
@book(DLMR13,
 author       = {M. Dumas and La Rosa, M. and J. Mendling and H. A. Reijers},
 year         = {2013},
 title        = {{Fundamentals of Business Process Management}},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-33143-5},
)
@inproceedings(Fahl19,
 author       = {D. Fahland},
 year         = {2019},
 title        = {Describing Behavior of Processes with Many-to-Many Interactions},
 booktitle    = {Proc.\ of {PETRI NETS}},
 series       = {LNCS},
 volume       = {11522},
 publisher    = {Springer},
 pages        = {3--24},
 doi          = {10.1007/978-3-030-21571-2\_1},
)
@inproceedings(FlanaganQ02,
 author       = {C. Flanagan and S. Qadeer},
 year         = {2002},
 title        = {Predicate abstraction for software verification},
 booktitle    = {Proc. of {POPL}},
 pages        = {191--202},
 doi          = {10.1145/503272.503291},
)
@inproceedings(ijcar08,
 author       = {S. Ghilardi and E. Nicolini and S. Ranise and D. Zucchelli},
 year         = {2008},
 title        = {Towards {SMT} Model Checking of Array-Based Systems},
 booktitle    = {Proc.\ of {IJCAR}},
 pages        = {67--82},
 doi          = {10.1007/978-3-540-71070-7\_6},
)
@article(lmcs,
 author       = {S. Ghilardi and S. Ranise},
 year         = {2010},
 title        = {Backward Reachability of Array-based Systems by {SMT} Solving: Termination and Invariant Synthesis},
 journal      = {Logical Methods in Computer Science},
 volume       = {6},
 number       = {4},
 doi          = {10.2168/LMCS-6(4:10)2010},
)
@misc(OMG2013,
 author       = {Object Management Group},
 year         = {2013},
 title        = {OMG Unified Modeling Language 2.5},
 note         = {Http://www.omg.com/uml/},
)
@inproceedings(GM,
 author       = {S. Gulwani and M. Musuvathi},
 year         = {2008},
 title        = {Cover Algorithms and Their Combination},
 booktitle    = {Proc.\ of {ESOP}, Held as Part of {ETAPS}},
 pages        = {193--207},
 doi          = {10.1007/978-3-540-78739-6\_16},
)
@inproceedings(BCDD*12,
 author       = {B. Bagheri Hariri and D. Calvanese and De Giacomo, G. and De Masellis, R. and P. Felli and M. Montali},
 year         = {2012},
 title        = {Verification of Description Logic Knowledge and Action Bases},
 booktitle    = {Proc.\ ECAI},
 pages        = {103--108},
 doi          = {10.3233/978-1-61499-098-7-103},
)
@inproceedings(pdr,
 author       = {K. Hoder and Bj{\o}rner, Nikolaj},
 year         = {2012},
 title        = {Generalized Property Directed Reachability},
 booktitle    = {Proc.\ of {SAT}},
 pages        = {157--171},
 doi          = {10.1007/978-3-642-31612-8\_13},
)
@inproceedings(voronkov,
 author       = {L. Kov{\'{a}}cs and A. Voronkov},
 year         = {2009},
 title        = {Interpolation and Symbol Elimination},
 booktitle    = {Proc.\ of {CADE}},
 pages        = {199--213},
 doi          = {10.1007/978-3-642-02959-2\_17},
)
@inproceedings(Las16,
 author       = {S. Lasota},
 year         = {2016},
 title        = {Decidability Border for Petri Nets with Data: {WQO} Dichotomy Conjecture},
 booktitle    = {Proc.\ of {PETRI NETS}},
 series       = {LNCS},
 volume       = {9698},
 publisher    = {Springer},
 pages        = {20--36},
 doi          = {10.1007/978-3-319-39086-4\_3},
)
@article(verifas,
 author       = {Y. Li and A. Deutsch and V. Vianu},
 year         = {2017},
 title        = {{VERIFAS:} {A} Practical Verifier for Artifact Systems},
 journal      = {{PVLDB}},
 volume       = {11},
 number       = {3},
 pages        = {283--296},
 doi          = {10.14778/3157794.3157798},
)
@inproceedings(McMillan06,
 author       = {K.L. McMillan},
 year         = {2006},
 title        = {{Lazy Abstraction with Interpolants}},
 booktitle    = {Proc.\ of {CAV}},
 pages        = {123--136},
 doi          = {10.1007/11817963\_14},
)
@article(MonR17,
 author       = {M. Montali and A. Rivkin},
 year         = {2017},
 title        = {{DB-Nets}: on The Marriage of Colored {Petri} {Nets} and Relational Databases},
 journal      = {TOPNOC},
 volume       = {12},
 pages        = {91--118},
 doi          = {10.1007/978-3-662-55862-1\_5},
)
@book(OMG2009,
 author       = {{OMG}},
 year         = {2009},
 title        = {{Business Process Model and Notation (BPMN) - Version 2.0, Beta 1}},
)
@inproceedings(padon,
 author       = {O. Padon and N. Immerman and S. Shoham and A. Karbyshev and M. Sagiv},
 year         = {2016},
 title        = {Decidability of inferring inductive invariants},
 booktitle    = {Proc.\ of {POPL}},
 pages        = {217--231},
 doi          = {10.1145/2837614.2837640},
)
@inproceedings(Reic12,
 author       = {M. Reichert},
 year         = {2012},
 title        = {Process and Data: {T}wo Sides of the Same Coin?},
 booktitle    = {Proc.\ of the On the Move Confederated Int.\ Conf.\ (OTM~2012)},
 series       = {LNCS},
 volume       = {7565},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-33606-5\_2},
)
@inproceedings(Rich10,
 author       = {C. Richardson},
 year         = {2010},
 title        = {Warning: Don't Assume Your Business Processes Use Master Data},
 booktitle    = {Proc.\ of BPM},
 series       = {LNCS},
 volume       = {6336},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-15618-2\_3},
)
@article(RVFE11,
 author       = {Rosa-Velardo, F. and D. de Frutos-Escrig},
 year         = {2011},
 title        = {Decidability and complexity of Petri nets with unordered data},
 journal      = {Theor. Comput. Sci.},
 volume       = {412},
 number       = {34},
 pages        = {4439--4451},
 doi          = {10.1016/j.tcs.2011.05.007},
)
@inproceedings(SS16,
 author       = {Sofronie-Stokkermans, V.},
 year         = {2016},
 title        = {On Interpolation and Symbol Elimination in Theory Extensions.},
 booktitle    = {Proc.\ of {IJCAR}},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer},
 pages        = {273--289},
 doi          = {10.1007/978-3-319-40229-1\_19},
)
@inproceedings(Vian09,
 author       = {V. Vianu},
 year         = {2009},
 title        = {Automatic Verification of Database-Driven Systems: a New Frontier},
 booktitle    = {Proc.\ of ICDT},
 pages        = {1--13},
 doi          = {10.1145/1514894.1514896},
)