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...

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thomas Wies
• Keywords: Algebraic Data Types, Data Structure Logic, Decidable Logics, Software Engineering, VMCAI 2010