In the last two decades, Craig interpolation has emerged as a powerful tool in formal verification. Interpolants are largely exploited as an eficient method to approximate the reachable states and for invariant synthesis. In this survey, we report recent results on “stronger interpolants”, called uniform interpolants, and we discuss how they can be used to develop efective techniques for computing the reachable states in an exact way. Uniform interpolants can be eficiently computed when verifying data-aware processes, where the control flow of a (business) process can interact with a data storage. This is significant since integrating data and processes is a long-standing problem in business process management.
In this survey, we report recent results on the use of uniform interpolants (UIs) in automated
reasoning [
From a more applied perspective, a huge body of research has been dedicated to the problem of reconciling data and business process management (BPM [19]) within contemporary organizations [20, 21, 22]. More specifically, in the BPM context it has become more and more important to study multi-perspective models that do not just conceptually account for the control-flow dimension of business processes, but also consider the interplay with data [ 23, 14]: in contrast with abstract DAPs, these models are more focused on concrete processes as they are interpreted by stakeholders and BPM practitioners. One important challenge that naturally arises is how to formally verify such business processes enriched with data [24, 23]: since they are complex infinite-state systems, this requires to develop sophisticated symbolic techniques. The Problem of Quantifiers. Verification of infinite-state systems, and in particular of DAPs, when studied in declarative terms, requires to symbolically represent transitions and reachable states: contrary to finite-state model checking [ 25], an explicit and exhaustive exploration of the state space is not possible, because of the presence of infinitely many states.
Several techniques based on SMT have been studied to attack the general problem: for instance, there are prominent methods that are based on forward reachability, such as K-induction [26], or on backward reachability [27]. Methods based on backward reachability symbolically explore the state space starting from ‘unsafe’ states via an iterative computation of predecessors (i.e., the (pre-)image), until a fixpoint is reached or the initial state(s) are intersected. There exist various SMT-based model checkers implementing these methods (e.g., Kind 2 [28] or mcmt [29]).
In many first-order (FO) declarative formalisms (e.g., [ 27]), sets of states are represented using
quantifier-free logical formulae, called state formulae: the content of variables in a state formula
characterizes the global state of the system and may change during its evolution. The verification
procedure symbolically computes reachable sets of states, which should be represented again as
state formulae: indeed, images are intended to describe sets of states, and, as such, they should
be quantifier-free . Reachable sets of states need to be manipulated, because in general are not
described by state formulae: this is because, when computing images, FO (mostly, existential)
quantifiers may be introduced by the transitions, which are usually quantified formulae. For
instance, this is the case of DAP models, whose transitions contain as guards existential queries
over a relational database [
Dealing with quantifiers is a genuine problem when using frameworks based on SMT. For instance, declarative versions of backward reachability [31, 27] require discharging to SMT solvers proof obligations in the form of satisfiability tests for quantified formulae with a restricted shape. Although SMT solvers natively reason about the quantifier-free fragments, FO quantifiers can be in some cases handled by instantiation [27], whereas in others [32], where quantifiers range over specific real values involving light forms of arithmetic, proper QE can be used [33].
To summmarize, the precise computation of the set of reachable states can be in principle performed via proper quantifier elimination. However, quantifier elimination is not always possible in generic FO theories, and, when available, is in many cases computationally intractable: for instance, this is the case of arithmetical theories. In order to cope with this problem, other methods for symbol elimination (e.g., predicate abstraction [34, 35] or ordinary (Craig) interpolation [36, 37, 38]) have been investigated, which do not compute precise images, but perform an approximation of the reachable states: this implies that images can contain ‘spurious elements’, i.e., states that are not properly reachable in one step. Nevertheless, these methods are quite successful and computationally eficient. The main limitation is that they usually require refinement techniques to handle the spurious traces possibly produced by the approximation.
We now remark how in significant cases (e.g., data-aware business processes), approximating
methods can be abandoned in favor of exact methods that have the merits of both computing
precise images and remaining computationally tractable (i.e., in polytime). These methods are
based on the use of uniform interpolants, a strong form of interpolants having strict relationships
with quantifier elimination performed in richer theories called model completions. We clarify
why model completions come to the picture and how they are related to uniform interpolation.
Model-Theoretic Algebra and Model Completions An FO theory has quantifier
elimination if for every formula in the signature Σ of there is a quantifier-free formula ′ s.t.
is -equivalent to ′. Eliminating quantifiers from a generic FO formula can be equivalently
formulated as the problem of eliminating existential quantifiers from constraints. Elimination
of existentials has an interesting interpretation: it can be seen as the logical counterpart of
ifnding witnesses, i.e., solutions, to suitable systems of logical “equations and/or disequalities”.
Model-theoretic algebra, since the pioneering work by Robinson [
The central notion is that of existentially closed model. A quantifier-free formula with parameters in a model is solvable if there is an extension ′ of where the formula is satisfied. A model is existentially closed if any solvable formula already has a solution in itself. This is not FO definable in general. However, in significant cases, the class of existentially closed models of are exactly the models of another FO theory * , called model completion [40] of . Formally, a universal theory has a model completion if there is a stronger theory * ⊇ (still within the same signature Σ of ) s. t.: (i) every Σ -constraint satisfiable in a model of is satisfiable in a model of * ; (ii) * eliminates quantifiers . The theory * , if it exists, is unique. In model completions, QE holds, even in case it does not in . The model completion of a theory identifies the class of the models where all satisfiable existential statements can be satisfied .
In declarative approaches to verification of infinite-state systems, the runs of a system that are
‘analyzed’ by image computation are identified with certain definable paths in the models of a
suitable theory : e.g., in the case of DAP models, the theory formalizes the relational database
that is queried and modified by the process [
Model completions become the crucial tool to exploit: one of the main results from [
For every pair of -formulae (, ) and (, ) s.t. ⊢ , a UI of is in particular an ordinary (Craig) interpolant for the pair (, ) [41]. Hence, whenever UIs exist, one can compute an ordinary interpolant for ⊢ in a way that is independent of , i.e., uniformly.
UIs were originally investigated in non-classical logics, since the work by Pitts [42]. They are stronger than ordinary interpolants: even in case Craig interpolants exist, UIs may not exist. Since the nineties, they have been extensively studied in a large literature (e.g., [43, 44, 45]).
Recently, the automated reasoning community has developed an increasing interest in UIs,
where is the quantifier-free fragment of an FO theory : from now on, we restrict our
attention to this case. This is witnessed by various talks by Kapur (FLoC 2010, ISCAS 2013-14,
SCS 2017 [46]), as well as by Gulwani and Musuvathi in [47], where UIs are called covers.
The use of UIs in model checking to compute exact images of states was first shown in that
work, and then further motivated by DAP verification [
DAP verification also suggests the study of UI transfer to combined theories: it is natural
to consider the combination of theories accounting for diferent datatypes contained in the
persistent storage [
This work is partially supported by the Italian Ministry of University and Research under the PRIN program, grant B87G22000450001 (PINPOINT), and by the Free University of BozenBolzano with the SMART-APP and ADAPTERS projects. [13] G. D. Giacomo, X. Oriol, M. Estañol, E. Teniente, Linking data and BPMN processes to achieve executable models, in: Proc. of CAiSE, LNCS, Springer, 2017, pp. 612–628. [14] D. Calvanese, G. De Giacomo, M. Montali, Foundations of data-aware process analysis: A database theory perspective, in: Proceedings of PODS 2013, 2013, pp. 1–12. [15] B. Bagheri Hariri, D. Calvanese, G. De Giacomo, A. Deutsch, M. Montali, Verification of relational data-centric dynamic systems with external services, in: Proceedings of PODS 2013, 2013, pp. 163–174. [16] A. Deutsch, R. Hull, Y. Li, V. Vianu, Automatic verification of database-centric systems,
ACM SIGLOG News 5 (2018) 37–56. [17] A. Deutsch, Y. Li, V. Vianu, Verification of hierarchical artifact systems, in: Proceedings of
PODS 2016, 2016, pp. 179–194. [18] A. Deutsch, Y. Li, V. Vianu, Verification of hierarchical artifact systems, ACM Transactions on Database Systems 44 (2019) 12:1–12:68. [19] M. Dumas, M. L. Rosa, J. Mendling, H. A. Reijers, Fundamentals of Business Process
Management, Second Edition, Springer, 2018. [20] C. Richardson, Warning: Don’t assume your business processes use master data, in:
Proceedings of BPM 2010, volume 6336 of LNCS, Springer, 2010, pp. 11–12. [21] M. Dumas, On the convergence of data and process engineering, in: Proceedings of ADBIS 2011, volume 6909 of LNCS, Springer, 2011, pp. 19–26. [22] M. Reichert, Process and data: Two sides of the same coin?, in: Proceedings of OTM 2012, volume 7565 of LNCS, Springer, 2012, pp. 2–19. [23] E. Damaggio, A. Deutsch, R. Hull, V. Vianu, Automatic verification of data-centric business processes, in: Proceedings of BPM 2011, volume 6896 of LNCS, Springer, 2011, pp. 3–16. [24] A. Deutsch, R. Hull, F. Patrizi, V. Vianu, Automatic verification of data-centric business processes, in: Proceedings of ICDT 2009, 2009, pp. 252–267. [25] E. M. Clarke, O. Grumberg, D. A. Peled, Model checking, MIT Press, 2001. [26] M. Sheeran, S. Singh, G. Stålmarck, Checking safety properties using induction and a SAT-solver, in: Proceedings of FMCAD 2000, volume 1954 of LNCS, Springer, 2000, pp. 108–125. [27] S. Ghilardi, S. Ranise, Backward reachability of array-based systems by SMT solving:
Termination and invariant synthesis, Logical Methods in Computer Science 6 (2010). [28] A. Champion, A. Mebsout, C. Sticksel, C. Tinelli, The Kind 2 model checker, in: Proceedings of CAV 2016, volume 9780 of LNCS, Springer, 2016, pp. 510–517. [29] S. Ghilardi, S. Ranise, MCMT: A model checker modulo theories, in: Proceedings of IJCAR 2010, volume 6173 of LNCS (LNAI), Springer, 2010, pp. 22–29. [30] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, Y. Zhu, Bounded model checking, Adv. Comput. 58 (2003) 117–148. URL: https://doi.org/10.1016/S0065-2458(03)58003-2. doi:10.1016/S0065-2458(03)58003-2. [31] S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli, Towards SMT model checking of arraybased systems, in: Proceedings of IJCAR 2008, volume 5195 of LNCS (LNAI), Springer, 2008, pp. 67–82. [32] F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, N. Sharygina, An extension of lazy abstraction with interpolation for programs with arrays, Formal Methods in System Design 45 (2014) 63–109. [33] D. C. Cooper, Theorem proving in arithmetic without multiplication., in: Machine
Intelligence, volume 7, Edinburgh University Press, 1972, pp. 91–100. [34] R. Jhala, R. Majumdar, Software model checking, ACM Comput. Surv. 41 (2009) 21:1–21:54. [35] R. Jhala, A. Podelski, A. Rybalchenko, Predicate abstraction for program verification, in:
Handbook of Model Checking, Springer, 2018, pp. 447–491. [36] K. L. McMillan, Interpolation and SAT-Based Model Checking, in: Proceedings of CAV 2003, volume 2725 of LNCS, Springer, 2003, pp. 1–13. [37] K. L. McMillan, Lazy Abstraction with Interpolants, in: Proceedings of CAV 2006, volume 4144 of LNCS, Springer, 2006, pp. 123–136. [38] L. Kovács, A. Voronkov, Interpolation and symbol elimination, in: Proceedings of CADE 2009, volume 5663 of LNCS (LNAI), Springer, 2009, pp. 199–213. [39] A. Robinson, On the metamathematics of algebra, Studies in Logic and the Foundations of
Mathematics, North-Holland Publishing Co., Amsterdam, 1951. [40] C.-C. Chang, J. H. Keisler, Model Theory, third ed., North-Holland Publishing Co.,
Amsterdam-London, 1990. [41] W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, Journal of Symbolic Logic 22 (1957) 269–285. [42] A. M. Pitts, On an interpretation of second order quantification in first order intuitionistic propositional logic, Journal of Symbolic Logic 57 (1992) 33–52. [43] S. Ghilardi, M. Zawadowski, Sheaves, games, and model completions, volume 14 of Trends in Logic—Studia Logica Library, Kluwer Academic Publishers, Dordrecht, 2002. [44] T. Kowalski, G. Metcalfe, Uniform interpolation and coherence, Annals of Pure and
Applied Logic 170 (2019) 825–841. [45] G. Metcalfe, L. Reggio, Model completions for universal classes of algebras: necessary and suficient conditions, Journal of Symbolic Logic (2022) 1–34. [46] D. Kapur, Nonlinear polynomials, interpolants and invariant generation for system analysis, in: Proceedings of SC-Square 2017 (co-located with ISSAC), volume 1974, CEUR Workshop Proceedings, 2017. [47] S. Gulwani, M. Musuvathi, Cover algorithms and their combination, in: Proceedings of
ESOP 2008, volume 4960 of LNCS, Springer, 2008, pp. 193–207. [48] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Model completeness, covers and superposition, in: Proceedings of CADE 2019, volume 11716 of LNCS (LNAI), Springer, 2019, pp. 142–160. [49] S. Ghilardi, A. Gianola, D. Kapur, Uniform interpolants in EUF: Algorithms using DAGrepresentations, Logical Methods in Computer Science 18 (2022). [50] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Combined Covers and Beth Definability, in: Proceedings of IJCAR 2020, volume 12166 of LNCS (LNAI), Springer, 2020, pp. 181–200. [51] G. Yorsh, M. Musuvathi, A combination method for generating interpolants, in: Proceedings of CADE 2005, volume 3632 of LNCS, Springer, 2005, pp. 353–368.