---
res:
  bibo_abstract:
  - 'Techniques such as verification condition generation, predicate abstraction,
    and expressive type systems reduce software verification to proving formulas in
    expressive logics. Programs and their specifications often make use of data structures
    such as sets, multisets, algebraic data types, or graphs. Consequently, formulas
    generated from verification also involve such data structures. To automate the
    proofs of such formulas we propose a logic (a “calculus”) of such data structures.
    We build the calculus by starting from decidable logics of individual data structures,
    and connecting them through functions and sets, in ways that go beyond the frameworks
    such as Nelson-Oppen. The result are new decidable logics that can simultaneously
    specify properties of different kinds of data structures and overcome the limitations
    of the individual logics. Several of our decidable logics include abstraction
    functions that map a data structure into its more abstract view (a tree into a
    multiset, a multiset into a set), into a numerical quantity (the size or the height),
    or into the truth value of a candidate data structure invariant (sortedness, or
    the heap property). For algebraic data types, we identify an asymptotic many-to-one
    condition on the abstraction function that guarantees the existence of a decision
    procedure. In addition to the combination based on abstraction functions, we can
    combine multiple data structure theories if they all reduce to the same data structure
    logic. As an instance of this approach, we describe a decidable logic whose formulas
    are propositional combinations of formulas in: weak monadic second-order logic
    of two successors, two-variable logic with counting, multiset algebra with Presburger
    arithmetic, the Bernays-Schönfinkel-Ramsey class of first-order logic, and the
    logic of algebraic data types with the set content function. The subformulas in
    this combination can share common variables that refer to sets of objects along
    with the common set algebra operations. Such sound and complete combination is
    possible because the relations on sets definable in the component logics are all
    expressible in Boolean Algebra with Presburger Arithmetic. Presburger arithmetic
    and its new extensions play an important role in our decidability results. In
    several cases, when we combine logics that belong to NP, we can prove the satisfiability
    for the combined logic is still in NP.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Viktor
      foaf_name: Kuncak, Viktor
      foaf_surname: Kuncak
  - foaf_Person:
      foaf_givenName: Ruzica
      foaf_name: Piskac, Ruzica
      foaf_surname: Piskac
  - foaf_Person:
      foaf_givenName: Philippe
      foaf_name: Suter, Philippe
      foaf_surname: Suter
  - foaf_Person:
      foaf_givenName: Thomas
      foaf_name: Wies, Thomas
      foaf_surname: Wies
      foaf_workInfoHomepage: http://www.librecat.org/personId=447BFB88-F248-11E8-B48F-1D18A9856A87
  bibo_doi: 10.1007/978-3-642-11319-2_6
  bibo_volume: 5944
  dct_date: 2010^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Building a calculus of data structures@
...