Hi everyone,
I will be giving a practice job talk "Abstract Interpretation Over
Bitvectors" this Monday in room 2310. It will help a lot if you attend
and critique the talk.
Abstract: "Abstract interpretation is a method to automatically verify a
program by soundly abstracting the concrete executions of the program to
elements in an abstract domain, and checking the correctness guarantees
using the abstraction. However, traditional abstract domains treat the
machine integers as mathematical integers. As a result, the conclusions
drawn from such an abstract interpretation are, in general, unsound. We
present sound abstraction techniques and abstract-domain frameworks that
faithfully model bit-vector semantics. We focus on numerical abstract
domains for bitvectors, which can provide equality and inequality
invariants. First, I present a new abstract-domain framework, named
Affine-Transformers Abstraction (ATA), that is capable of expressing a
certain class of disjunctions over bit-vector-sound equality
constraints. This framework can be instantiated with any relational or
non-relational base abstract domain over bitvectors. Then, I present an
abstract-domain framework, named Bit-Vector-Sound Finite Disjunctive
(BVSFD), that takes an abstract domain that is sound with respect to
mathematical integers, and creates an abstract domain whose operations
and abstract transformers are sound with respect to machine integers."
Thanks,
Tushar Sharma
|