Solving bitvectors with MCSAT: explanations from bits and pieces
type: Item
instance of: scholarly article
title: Solving bitvectors with MCSAT: explanations from bits and pieces
DOI: 10.1007/978-3-030-51074-9_7
author: Stéphane Graham-Lengrand
author: Dejan Jovanović
author: Bruno Dutertre
publication date: 2022-11-09T00:00:00Z
full work available at URL: https://arxiv.org/abs/2004.07940
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7614509
describes a project that uses: SIMPLIFY
describes a project that uses: Boolector
describes a project that uses: SMT-LIB
describes a project that uses: Yices
describes a project that uses: GitHub
MaRDI profile type: Publication
OpenAlex ID: W3038318403
cites work: Conflict-driven satisfiability for theory combination: transition system and completeness
cites work: Satisfiability modulo theories and assignments
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Sharpening constraint programming approaches for bit-vector theory
cites work: Simplify: a theorem prover for program checking
cites work: Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
cites work: Computer aided verification. 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18--22, 2014. Proceedings
cites work: A layered algorithm for quantifier elimination from linear modular constraints
cites work: Solving Nonlinear Integer Arithmetic with MCSAT
cites work: Decision procedures. An algorithmic point of view
cites work: Q5503674
cites work: A Model-Constructing Satisfiability Calculus
cites work: Solving quantified bit-vectors using invertibility conditions
cites work: Solving SAT and SAT Modulo Theories
cites work: Handbook of automated reasoning. In 2 vols
cites work: Deciding Bit-Vector Formulas with mcSAT
description: scientific article; zbMATH DE number 7614509