CP 2016 has ended
Back To Schedule
Monday, September 5 • 13:30 - 14:05
CP meets Verification - Invited talk: Constraint Satisfaction over Bit-Vectors
    See presentations
Reasoning over bit-vectors arises in a variety of applications in verification and cryptography. This talk considers a bit-vector domain for constraint programming and its associated filtering algorithms. The domain supports all the traditional bit operations and correctly models modulo-arithmetic and overflows. The domain implementation uses bit operations of the underlying architecture, avoiding the drawback of a bit-blasting approach. The filtering algorithms implement either domain consistency on the bit-vector domain or bit consistency. Filtering algorithms for logical and structural constraints typically run in constant time, while arithmetic constraints such as addition run in time linear in the size of the bit-vectors. The talk will discuss how to channel bit-vector variables with an integer variable and how to make use of the infrastructure to tackle problems commonly found in the Bit Vector Theory of the SMT-LIB benchmark suite. This is a joint work with P. Van Hentenryck (U. Michigan) , G. Johnson (U. Connecticut).

avatar for Laurent Michel

Laurent Michel

Associate Professor, University of Connecticut
Laurent's primary research interests lie at the intersection of Programming Language and Combinatorial Optimization. His efforts are directed to the construction of software tools that considerably simplify the development of complex application (most belong to the NP class) for discrete... Read More →

Monday September 5, 2016 13:30 - 14:05
B202 Bosco building

Attendees (3)