[pl-seminar] REMINDER: VMCAI practice talk at noon in 4310 CS (Donuts available)

[Tushar Sharma <tsharma@xxxxxxxxxxx>]

On 1/9/2017 11:17 AM, Tushar Sharma wrote:
> HI,
>
> I will be giving VMCAI practice talk tommorrow (Tuesday, Jan 10) at 
> noon in 4310 CS.
> Title: Sound Bit-Precise Numerical Domains
>
> Abstract: This paper tackles the challenge of creating a numerical 
> abstract
> domain that can identify affine-inequality invariants while handling
> overflow in arithmetic operations over bit-vector data-types. The
> paper describes the design and implementation of a class of new abstract
> domains, called the Bit-Vector-Sound, Finite-Disjunctive (BVSFD) domains.
> We introduce a framework that takes an abstract domain A that
> is sound with respect to mathematical integers and creates an abstract
> domain BVS(A) whose operations and abstract transformers are sound
> with respect to machine integers. We also describe how to create abstract
> transformers for BVS(A) that are sound with respect to machine
> arithmetic. The abstract transformers make use of an operation
> WRAP(av; v)|where av \in A and v is a set of program variables|which
> performs wraparound in av for the variables in v.
> To reduce the loss of precision from WRAP, we use finite disjunctions
> of BVS(A) values. The constructor of finite-disjunctive domains, FD_k(,
> is parameterized by k, the maximum number of disjunctions allowed.
> We instantiate the BVS(FD_k) framework using the abstract domain
> of polyhedra and octagons. Our experiments show that the analysis can
> prove 25% of the assertions in the SVCOMP loop benchmarks with k = 6,
> and 88% of the array-bounds checks in the SVCOMP array benchmarks
> with k = 4.
>
>
> Please attend and give feedback. I will provide some snacks.
>
> Thanks,
>
> Tushar
>
> _______________________________________________
> Pl-reading mailing list
> Pl-reading@xxxxxxxxxxx
> List Info: https://lists.cs.wisc.edu/mailman/listinfo/pl-reading
> Web-archive:  https://www-auth.cs.wisc.edu/lists/pl-reading/
> PL Reading: http://www.cs.wisc.edu/areas/pl/reading.php