Talks & Seminars
Title: Practical Quantifier Elimination for Linear Bitvector Arithmetic
Prof. Supratik Chakraborty, Dept. of CSE, IIT Bombay
Date & Time: March 13, 2013 16:30
Venue: Room # SIC 301, 03rd Floor, C Block, Department of Computer Science and Engineering, Kanwal Rekhi Building
Reasoning about fixed width bit-vectors (as opposed to reasoning about integers or reals) is important in the formal verification and analysis of software and hardware systems that use fixed-width words in the underlying machine architecture. While restricting the domain to fixed width bit-vectors renders all interesting problems decidable, the worst-case complexities may still be high, and one needs to exercise care in designing algorithms that scale to problems of practical size. In this talk, we look at the problem of quantifier elimination for linear arithmetic expressions, a key operation in verification, automated synthesis and analysis of important classes of software and hardware systems. We present a layered algorithm for scalable quantifier elimination from Boolean combinations of linear bitvector arithmetic expressions. Our algorithm invokes cheaper, relatively less complete heuristics initially, and invokes more expensive and complete techniques only when needed. We present a substitution based heuristic and a counting based heuristic that are extremely efficient and succeed in eliminating almost all quantifiers in an extensive set of benchmarks from the public-domain. To handle cases that are not amenable to these heuristics, we also present an adaptation of the classical Fourier-Motzkin quantifier elimination algorithm for reals to linear bitvector arithmetic. While this is an expensive step, our experiments indicate that this is invoked in a very small fraction of cases. Our experiments clearly show that a layered approach with carefully designed heuristics lends both precision and scalability to bit-precise quantifier elimination. We are currently working on extending this work to eliminating quantifiers from non-linear bit-vector inequalities and also for combinations of bit-vector theories.
Speaker Profile:
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback