Abstract
This paper shows how all different constraints
(ADCs) over bit-vectors can be handled within a SAT solver.
It also contains encouraging experimental results in applying
this technique to encode simple path constraints in bounded
model checking. Finally, we present a new compact encoding
of equalities and inequalities over bit-vectors in CNF.
| Original language | English |
|---|---|
| Title of host publication | Proc. 8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08) |
| Publisher | IEEE |
| Number of pages | 4 |
| ISBN (Print) | 978-1-4244-2735-2 |
| Publication status | Published - 2008 |
Fields of science
- 102 Computer Sciences