Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Sun 15 Jan 2017 17:00 - 17:30 at Amphitheater 44 - Decision procedures Chair(s): Andreas Podelski

SMT solvers for the theory of fixed-width bit-vectors are widely used. Bit-vector formulas often involve word-level arithmetic operations. Empirical evidence shows that bit-vector formulas with multiplication are often hard for SMT solvers to reason about. Therefore, it is important that an SMT solver uses all the structure available in the problem, including the word-level reasoning. Sometimes multiplication operators are decomposed and implemented in alternative ways, and the solver fails to identify the word-level multiplication operation. In this paper, we present a pre-processing heuristic that identifies the decomposed multipliers, and adds special assertions to the input formula that encodes equivalence of the decomposed multiplication and the word-level multiplication. The pre-processed formulas are then solved using an available solver. We have implemented our pre-processing algorithms in the rewriting engine of Z3 and applied these on a suite of benchmarks. Our experiments with three state-of-the-art SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.

Sun 15 Jan
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30: VMCAI - Decision procedures at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany
VMCAI-2017-papers16:00 - 16:30
Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences
File Attached
VMCAI-2017-papers16:30 - 17:00
Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-Alpes
File Attached
VMCAI-2017-papers17:00 - 17:30
Supratik ChakrabortyIIT Bombay, Ashutosh Gupta, Rahul JainTata Institute of Fundamental Research
File Attached