LARA

This is an old revision of the document!

Fixed-Width Bitvectors

Bitvector: integer from some finite inteval of length $2^n$

Example: $[0,2^{32}-1]$

Logic on bitvectors.

  • formulas for +.

We can reduce reasoning on bitvectors to reasoning in propositional logic.

Application:

  • exact reasoning about Java integers
  • finding counterexamples for formulas over unbounded integers