Matching Multiplications in Bit-Vector Formulas

DOI10.1007/978-3-319-52234-0_8zbMath1484.68098arXiv1611.10146OpenAlexW2558223845MaRDI QIDQ2961559

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)

Related Items

Matching Multiplications in Bit-Vector Formulas, Symbolic trajectory evaluation for word-level verification: theory and implementation

Uses Software

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

Cites Work

• Symbolic trajectory evaluation for word-level verification: theory and implementation
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Matching Multiplications in Bit-Vector Formulas
• A Proof of the Modified Booth's Algorithm for Multiplication
• The Strategy Challenge in SMT Solving
• Tools and Algorithms for the Construction and Analysis of Systems
• Majority Gate Networks