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