Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Mon 16 Jan 2017 10:30 - 11:00 at Amphitheater 44 - Numerical domains Chair(s): Laure Gonnord

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 Domains(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 abstract operations 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 parametrized 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.

slides (bitprecisevmcai17.pdf)916KiB

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00: Numerical domainsVMCAI at Amphitheater 44
Chair(s): Laure GonnordUniversity of Lyon & LIP, France
10:30 - 11:00
Sound Bit-Precise Numerical Domains
Tushar SharmaUniversity of Wisconsin - Madison, USA, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.
File Attached
11:00 - 11:30
Efficient Elimination of Redundancies in Polyhedra using Raytracing
Media Attached File Attached
11:30 - 12:00
Finding Relevant Templates via the Principal Component Analysis
Yassamine SeladjiUniversity of Tlemcen
File Attached