Solving linear arithmetic with SAT-based model checking

Yakir Vizel, Alexander Nadel, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

We present LIAMC, a novel decision procedure for (quantifier-free) linear arithmetic over both integers modulo 2N (LIAn) and integers (LIA). There is no need to explain our motivation to design a new efficient decision procedure for the widely used LIA logic. A LIAn decision procedure can be extremely useful in the context of software (SW) verification. SW verification usually requires to reason about arithmetic constraints over finite integers. To that end, modern SW verification tools commonly use fixed-width bit-vector (BV) solvers. However, BV solvers' efficiency drops dramatically as the width increases. To solve the performance problem, LIA solvers are applied, but they are imprecise as they cannot handle integer overflow. An efficient LIAN solver would be the ideal solution in this context. Our decision procedure LIAMC is based on a transformation of linear arithmetic into safety verification. We treat integers as unbounded streams of bits over time. More precisely, for each input integer, the least significant bit (LSB) corresponds to time 0 in the corresponding stream, and the k-th bit corresponds to the bit received at time k. LIAMC then uses SAT-based model checking (SATMC) to solve the resulting problem. In order to achieve efficiency, LIAMC uses two forms of generalization. First, if it finds a formula to be unsatisfiable for width N, it tries to generalize this result for all the widths. Second, if LIAMC finds a formula to be satisfiable for width N, it tries to 'extend' and thus generalize the assignment to a wider target width. To evaluate LIAMC we used the QF-LIA subset of SMT-COMP'16, and ran two sets of experiments. First, we reinterpreted the QF-LIA over fixed-width bit-vectors of varying widths and compared LIAMC in LIAn mode to both Boolector and Z3. LIAMC solved the most satisfiable instances out of the three even for the shortest width 32. Second, we compared LIAMC to CVC4 and Z3 on the original QF-LIA benchmarks. LIAMC was able to solve many instances that had not been solved by the other solvers.

Original languageEnglish (US)
Title of host publicationProceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017
EditorsGeorg Weissenbacher, Daryl Stewart
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages47-54
Number of pages8
ISBN (Electronic)9780983567875
DOIs
StatePublished - Nov 8 2017
Event17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 - Vienna, Austria
Duration: Oct 2 2017Oct 6 2017

Publication series

NameProceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017

Other

Other17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017
CountryAustria
CityVienna
Period10/2/1710/6/17

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Solving linear arithmetic with SAT-based model checking'. Together they form a unique fingerprint.

Cite this