---
_id: '4572'
abstract:
- lang: eng
  text: 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.
acknowledgement: This research was sponsored in part by the grants NSF-CCF-0427202
  and NSF-CCF-0546170.
alternative_title:
- LNCS
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: '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.'
  ista: '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.'
  mla: 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>.
  short: D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, Springer, 2007,
    pp. 378–394.
conference:
  name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
date_created: 2018-12-11T12:09:32Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:48Z
day: '01'
doi: 10.1007/978-3-540-69738-1_27
extern: 1
intvolume: '      4349'
month: '01'
page: 378 - 394
publication_status: published
publisher: Springer
publist_id: '138'
quality_controlled: 0
status: public
title: Invariant synthesis for combined theories
type: conference
volume: 4349
year: '2007'
...