---
res:
  bibo_abstract:
  - 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Dirk
      foaf_name: Beyer, Dirk
      foaf_surname: Beyer
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Thomas Henzinger
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Ritankar
      foaf_name: Majumdar, Ritankar S
      foaf_surname: Majumdar
  - foaf_Person:
      foaf_givenName: Andrey
      foaf_name: Rybalchenko, Andrey
      foaf_surname: Rybalchenko
  bibo_doi: 10.1007/978-3-540-69738-1_27
  bibo_volume: 4349
  dct_date: 2007^xs_gYear
  dct_publisher: Springer@
  dct_title: Invariant synthesis for combined theories@
...