A Benders Decomposition Approach to Deciding Modular Linear Integer Arithmetic

No abstract is available for this paper.

• Publication year

  2017

• Venue

  International Conference on Theory and Applications of Satisfiability Testing

• Publication date

  2017-08-28

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-319-66263-3_24
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Deciding Bit-Vector Formulas with mcSAT

  2016influential reference
• A Bit-Vector Solver with Word-Level Propagation

  2016cited by this paper
• The SeaHorn Verification Framework

  2015cited by this paper
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic

  2014cited by this paper
• A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors

  2014cited by this paper
• The IntSat Method for Integer Linear Programming

  2014cited by this paper
• Yices 2.2

  2014cited by this paper
• Boolector 2.0

  2014cited by this paper
• The MathSAT5 SMT Solver

  2013cited by this paper
• Solving Difference Constraints over Modular Arithmetic

  2013cited by this paper
• Alloxan Induced Oxidative Stress and Impairment of Oxidative Defense System in rats

  2013cited by this paper
• Efficiently Solving Bit-Vector Problems Using Model Checkers

  2013cited by this paper
• The Strategy Challenge in SMT Solving

  2013cited by this paper
• More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding

  2013cited by this paper
• Constraint Satisfaction over Bit-Vectors

  2012cited by this paper
• An Alternative to SAT-Based Approaches for Bit-Vectors

  2010cited by this paper
• The SMT-LIB Standard Version 2.0

  2010cited by this paper
• Apron: A Library of Numerical Abstract Domains for Static Analysis

  2009cited by this paper
• Introduction to Algorithms, third edition

  2009cited by this paper
• Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays

  2009cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Modular difference logic is hard

  2008cited by this paper
• A Decision Procedure for Bit-Vectors and Arrays

  2007cited by this paper
• A Lazy and Layered SMT ( B V ) Solver for Hard Industrial Verification Problems ⋆

  2007cited by this paper
• A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems

  2007cited by this paper
• Software Abstractions - Logic, Language, and Analysis

  2006cited by this paper
• The ASTREÉ Analyzer

  2005cited by this paper
• A comparison of complete global optimization solvers

  2005cited by this paper
• Encoding RTL Constructs for MathSAT: a Preliminary Report

  2005cited by this paper
• Partitioning procedures for solving mixed-variables programming problems

  2005cited by this paper
• Safe bounds in linear and mixed-integer linear programming

  2004cited by this paper
• An efficient finite-domain constraint solver for circuits

  2004cited by this paper
• Logic-based Benders decomposition

  2003cited by this paper
• Functional verification for SystemC descriptions using constraint solving

  2002cited by this paper
• RTL-datapath verification using integer linear programming

  2002cited by this paper
• Introduction to algorithms

  1996cited by this paper
• Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming

  1995cited by this paper
• Partitioning procedures for solving mixed-variables programming problems

  1962cited by this paper
• AND T

  year unknowninfluential reference

• Bit-Precise Reasoning via Int-Blasting

  2022cites this paper
• Logic-Based Benders Decomposition for Large-Scale Optimization

  2019cites this paper