Matching multiplications in bit-vector formulas

DOI10.1007/978-3-319-52234-0_8MaRDI QIDQ2961559zbMATH OpenOpenAlexFDO

Authors Supratik Chakraborty, Ashutosh Gupta, Rahul Jain

Publication date 21 February 2017

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1611.10146

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not very efficient at reasoning about bit-vector formulas with multiplication. This is particularly true when multiplication operators are decomposed and represented in alternative ways in the formula.We present a pre-processing heuristic that identifies certain types of decomposed multipliers, and adds special assertions to the input formula encoding the equivalence of sub-terms to word-level multiplication. The pre-processed formulas are then solved using an SMT solver. Our experiments with three SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.

Recommendations

• Efficiently solving quantified bit-vector formulas
• Deciding Bit-Vector Arithmetic with Abstraction
• A bit-vector solver with word-level propagation
• Deciding Bit-Vector Formulas with mcSAT
• Abstraction of bit-vector operations for BDD-based SMT solvers

Cites work

• A Proof of the Modified Booth's Algorithm for Multiplication
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Majority Gate Networks
• Matching multiplications in bit-vector formulas
• Symbolic trajectory evaluation for word-level verification: theory and implementation
• The strategy challenge in SMT solving
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(3)

• Efficiently solving quantified bit-vector formulas
• Matching multiplications in bit-vector formulas
• Symbolic trajectory evaluation for word-level verification: theory and implementation

Describes a project that uses

Uses Software

• Boolector
• CUTE
• SMT-LIB
• z3
• DART
• Boogie
• CVC4
• CBMC

This page was built for publication: Matching multiplications in bit-vector formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2961559)