Differences
This shows you the differences between two versions of the page.
|
sav08:fixed-width_bitvectors [2008/03/12 22:12] vkuncak |
sav08:fixed-width_bitvectors [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== 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 | ||
| - | |||
| - | |||
| - | * [[http://www.springerlink.com/content/t57g3616p4756140/|Bitvectors and Arrays]] | ||