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