Priyank Kalla: Verification of Bit-Vector Arithmetic using Finite Integer Algebras

PRACTICALITIES

Lunch is served at 12:00 noon (register at this doodle at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

ABSTRACT

Finite-precision integer arithmetic plays an important role in many hardware and software systems, minimizing resource usage while maintaining necessary precision.  However, operating on these bit-vector (BV) data-types can introduce subtle, unforeseen errors, causing incorrect function or even security vulnerabilities.  With the widespread use of finite-precision arithmetic from multimedia DSP to embedded automotive control, it is imperative to devise new techniques to efficiently model and verify such systems at higher levels of abstractions --- raising the abstraction from bits to words, yet maintaining precision.

A bit-vector of size "m" represents integer values reduced "(mod 2^m)". Therefore, BV-arithmetic can be modeled as a system of polynomial functions over Z_{2^m}; and number-theoretic and algebraic techniques can be devised for verification. In this talk, I will describe decision procedures for verification of bit-vector arithmetic that lie at the cross-roads of number theory and commutative algebra --- such as canonical simplification of polynomial functions, Newton's p-adic iterations, etc. We will look at the challenge of making such techniques practical, and also discuss their potential for integration with SMT-solvers.

BIOGRAPHY

Priyank Kalla is an Associate Professor in the Electrical & Computer Engineering department at the Univ. of Utah. His areas of interests are in electronic design automation and hardware verification. He received the B.E. degree in Electronics from Sardar Patel University in India (1993) and M.S. and Ph.D. from the Univ. of Massachusetts Amherst in 1998 and 2002, respectively. He has worked with AMD K-7 and the DEC Alpha microprocessor CAD & Test groups. He's a recipient of the US NSF CAREER award and the ACM Trans. on Design Automation best paper award. He was the chair of IEEE technical committee on computer-aided network design and currently serves as an associate editor for IEEE Trans. on CAD.