[Documentation] The BMC algorithm. #3396
Conversation
johanneskloos
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
|
Ping @tautschnig - can you have a look at this section, please? |
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 6f3b712).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91241953
xbauch
left a comment
xbauch
left a comment
There was a problem hiding this comment.
Really like the examples. I'm not sure it was necessary to go that deep into bit-vectors, but now that it's there, I think it's good.
| We can then assert that `fac`=1 using | ||
| the propositional formula | ||
| `fac`<sub>63</sub> = 0 and ... and `fac`<sub>1</sub> = 0 and `fac`<sub>0</sub> = 1, | ||
| where we define the formula A = B as ''(A and B) or ((not A) and (not B))''. |
There was a problem hiding this comment.
I think we'd rather do ((not A) or B) and (A or (not B)) to be closer to CNF.
There was a problem hiding this comment.
Changed to (A or not B) and (B or not A) to save braces.
| mostly *propositional logic* and (fragments of) *first-order logic*. | ||
|
|
||
| In the following, we will quickly discuss propositional logic, in combination | ||
| with SAT solving, and show how to build a simple bounded model checker for |
There was a problem hiding this comment.
Why remove this restriction?
There was a problem hiding this comment.
My original intention was to show bounded model checking on code that's essentially a finite-state automaton, but that's actually not very helpful. Should I add the restriction back?
| In the following, we will quickly discuss propositional logic, in combination | ||
| with SAT solving, and show how to build a simple bounded model checker for | ||
| a finite-state program. Actual bounded model checking for software requires | ||
| with SAT solving, and show how to build a simple bounded model checker |
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 3314ed3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91378314
|
@johanneskloos, please squash the commits. |
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 33fac5d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91657871
6 participants
This extends the background concepts section with a description of the BMC algorithm. Review needed!
Documentation only commit: