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.

h1. [Ruzica Piskac|http://icwww.epfl.ch/~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.

{attachments:patterns=.*}