## Abstract

Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.

Original language | English |
---|---|

Title of host publication | Theory and Applications of Satisfiability Testing – SAT 2017 |

Subtitle of host publication | 20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings |

Editors | Serge Gaspers, Toby Walsh |

Place of Publication | Cham Switzerland |

Publisher | Springer |

Pages | 380-397 |

Number of pages | 18 |

ISBN (Electronic) | 9783319662633 |

ISBN (Print) | 9783319662626 |

DOIs | |

Publication status | Published - 2017 |

Externally published | Yes |

Event | International Conference on Theory and Applications of Satisfiability Testing 2017 - Melbourne, Australia Duration: 28 Aug 2017 → 1 Sep 2017 Conference number: 20th http://sat2017.gitlab.io/ |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 10491 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | International Conference on Theory and Applications of Satisfiability Testing 2017 |
---|---|

Abbreviated title | SAT 2017 |

Country | Australia |

City | Melbourne |

Period | 28/08/17 → 1/09/17 |

Internet address |