SC Chapter 6 Bit Vectors
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 6 Bit Vectors
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 6 Bit Vectors
Kartei Details
| Karten | 24 |
|---|---|
| Sprache | English |
| Kategorie | Informatik |
| Stufe | Universität |
| Erstellt / Aktualisiert | 18.02.2017 / 27.02.2017 |
| Lizenzierung | Keine Angabe |
| Weblink |
https://card2brain.ch/box/20170218_sc_chapter_6_bit_vectors
|
| Einbinden |
<iframe src="https://card2brain.ch/box/20170218_sc_chapter_6_bit_vectors/embed" width="780" height="150" scrolling="no" frameborder="0"></iframe>
|
Why is bit vector logic (BVL) needed?
Because of bit-wise operation and arithmetic overflow in system-level software
What can happen for large software?
Formulas will become large
What are current implementations using BVL? [5]
1. CBMC
2. SATABS
3. F-Soft (NEC)
4. SATURN (Stanford, Aiken)
5. EXE (Stanford, Engler and Dill)
What are the syntax components of BVL? [5]
1. Operators op are + - * / << >> & | xor °
2. Terms t are t op t, identifier, ~t, constant c, a?t:t, t[c:c], ext(t)
3. Relations rel are = <
4. Atoms a are t rel t, Boolean-Identifier, t[c]
5. Formulas f are f \lor f, \neg f, atom
What is a semantic problem of BVL compared to N and R?
(x-y)>0 ↔ x>y does not hold for BVL
What are the semantic components of BVL? [3]
1. Vector x
2. Width
3. Encoding E
What are the characteristics of the vector x of BVL? [3]
1. Every entry x(i) or x_i is mapped to 0 or 1
2. Most left is highest index l-1
3. Most right is lowest index 0
What are possible encodings E of BVL? [4]
1. Binary U 2. two’s complement S 3. fixed-point and 4. floating-point
