### Abstract

We present LIAMC, a novel decision procedure for (quantifier-free) linear arithmetic over both integers modulo 2^{N} (LIA_{n}) 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 LIA_{n} 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 LIA_{N} 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 language | English (US) |
---|---|

Title of host publication | Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 |

Editors | Georg Weissenbacher, Daryl Stewart |

Publisher | Institute of Electrical and Electronics Engineers Inc. |

Pages | 47-54 |

Number of pages | 8 |

ISBN (Electronic) | 9780983567875 |

DOIs | |

State | Published - Nov 8 2017 |

Event | 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 - Vienna, Austria Duration: Oct 2 2017 → Oct 6 2017 |

### Publication series

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

### Other

Other | 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017 |
---|---|

Country | Austria |

City | Vienna |

Period | 10/2/17 → 10/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

*Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017*(pp. 47-54). [8102240] (Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.23919/FMCAD.2017.8102240