Building a Calculus of Data Structures

9 years 11 months ago
Building a Calculus of Data Structures
Abstract. Techniques such as verification condition generation, preditraction, 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. of our decidable logics include abstraction functions that map tructure into its more abstract view (a tree into a multiset, a multise...
Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thom
Added 05 Mar 2010
Updated 08 Mar 2010
Type Conference
Year 2010
Authors Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies
Comments (0)