conference paper published Dirk Beyer author Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 Ritankar Majumdar author Andrey Rybalchenko author VMCAI: Verification, Model Checking and Abstract Interpretation We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C. Springer2007 10.1007/978-3-540-69738-1_27 4349378 - 394 yes Beyer, D., Henzinger, T. A., Majumdar, R., &#38; Rybalchenko, A. (2007). Invariant synthesis for combined theories (Vol. 4349, pp. 378–394). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. <a href="https://doi.org/10.1007/978-3-540-69738-1_27">https://doi.org/10.1007/978-3-540-69738-1_27</a> Beyer, Dirk, Thomas A Henzinger, Ritankar Majumdar, and Andrey Rybalchenko. “Invariant Synthesis for Combined Theories,” 4349:378–94. Springer, 2007. <a href="https://doi.org/10.1007/978-3-540-69738-1_27">https://doi.org/10.1007/978-3-540-69738-1_27</a>. Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. 2007. Invariant synthesis for combined theories. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 4349, 378–394. Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Invariant synthesis for combined theories. In: Vol 4349. Springer; 2007:378-394. doi:<a href="https://doi.org/10.1007/978-3-540-69738-1_27">10.1007/978-3-540-69738-1_27</a> D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, “Invariant synthesis for combined theories,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, 2007, vol. 4349, pp. 378–394. Beyer, Dirk, et al. <i>Invariant Synthesis for Combined Theories</i>. Vol. 4349, Springer, 2007, pp. 378–94, doi:<a href="https://doi.org/10.1007/978-3-540-69738-1_27">10.1007/978-3-540-69738-1_27</a>. D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, Springer, 2007, pp. 378–394. 45722018-12-11T12:09:32Z2021-01-12T07:59:48Z