Calculus of Data Structures for Verification and Synthesis

We consider a calculus of data structures as away to extend reasoning about the numbers and functions with reasoning
about data structures such as lists, sets, trees, relations. Such constraints are derived either in software verification (finding an
input that crashes the program, or an invariant that proves the program correct) or in software synthesis (finding a program that satisfies the
given specification). In this talk I will describe a technique to reason about very expressive logics by connecting them through functions and
sets, in ways that go beyond frameworks such as Nelson-Oppen. I will also report on the use of decision procedures in software synthesis.

Ruzica Piskac, EPFL, Lausanne, Switzerland

Ruzica Piskac is a PhD candidate at EPFL, working under the supervision of Viktor Kuncak. Her primary research interests
are decision procedures, their combinations and applications in program verification and software synthesis.