Re: [pl-seminar] Practice Job Talk on Monday July 31st at noon (2310 CS)

[Tushar Sharma <tsharma@xxxxxxxxxxx>]

Reminder! The talk is at noon today in 2310 CS. There will be donuts!

Thanks,
Tushar

On 7/27/2017 10:26 AM, Tushar Sharma wrote:
> 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
> _______________________________________________
> Pl-seminar mailing list
> Pl-seminar@xxxxxxxxxxx
> https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar