---
_id: '4378'
abstract:
- lang: eng
  text: '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.'
alternative_title:
- LNCS
author:
- first_name: Viktor
  full_name: Kuncak, Viktor
  last_name: Kuncak
- first_name: Ruzica
  full_name: Piskac, Ruzica
  last_name: Piskac
- first_name: Philippe
  full_name: Suter, Philippe
  last_name: Suter
- first_name: Thomas
  full_name: Wies, Thomas
  id: 447BFB88-F248-11E8-B48F-1D18A9856A87
  last_name: Wies
citation:
  ama: 'Kuncak V, Piskac R, Suter P, Wies T. Building a calculus of data structures.
    In: Barthe G, Hermenegildo M, eds. Vol 5944. Springer; 2010:26-44. doi:<a href="https://doi.org/10.1007/978-3-642-11319-2_6">10.1007/978-3-642-11319-2_6</a>'
  apa: 'Kuncak, V., Piskac, R., Suter, P., &#38; Wies, T. (2010). Building a calculus
    of data structures. In G. Barthe &#38; M. Hermenegildo (Eds.) (Vol. 5944, pp.
    26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
    Madrid, Spain: Springer. <a href="https://doi.org/10.1007/978-3-642-11319-2_6">https://doi.org/10.1007/978-3-642-11319-2_6</a>'
  chicago: Kuncak, Viktor, Ruzica Piskac, Philippe Suter, and Thomas Wies. “Building
    a Calculus of Data Structures.” edited by Gilles Barthe and Manuel Hermenegildo,
    5944:26–44. Springer, 2010. <a href="https://doi.org/10.1007/978-3-642-11319-2_6">https://doi.org/10.1007/978-3-642-11319-2_6</a>.
  ieee: 'V. Kuncak, R. Piskac, P. Suter, and T. Wies, “Building a calculus of data
    structures,” presented at the VMCAI: Verification, Model Checking and Abstract
    Interpretation, Madrid, Spain, 2010, vol. 5944, pp. 26–44.'
  ista: 'Kuncak V, Piskac R, Suter P, Wies T. 2010. Building a calculus of data structures.
    VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944,
    26–44.'
  mla: Kuncak, Viktor, et al. <i>Building a Calculus of Data Structures</i>. Edited
    by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44,
    doi:<a href="https://doi.org/10.1007/978-3-642-11319-2_6">10.1007/978-3-642-11319-2_6</a>.
  short: V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo
    (Eds.), Springer, 2010, pp. 26–44.
conference:
  end_date: 2010-01-19
  location: Madrid, Spain
  name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
  start_date: 2010-01-17
date_created: 2018-12-11T12:08:33Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:31Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-11319-2_6
editor:
- first_name: Gilles
  full_name: Barthe, Gilles
  last_name: Barthe
- first_name: Manuel
  full_name: Hermenegildo, Manuel
  last_name: Hermenegildo
intvolume: '      5944'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://infoscience.epfl.ch/record/161290/
month: '01'
oa: 1
oa_version: Submitted Version
page: 26 - 44
publication_status: published
publisher: Springer
publist_id: '1081'
quality_controlled: '1'
scopus_import: 1
status: public
title: Building a calculus of data structures
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 5944
year: '2010'
...