[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? |
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
| 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.
| @@ -696,8 +696,8 @@ is to encode both the program and the set of states using an appropriate logic, | |||
| 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?
There was a problem hiding this comment.
@peterschrammel Any further comments?
| @@ -696,8 +696,8 @@ is to encode both the program and the set of states using an appropriate logic, | |||
| 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 | |||
| a finite-state program. Actual bounded model checking for software requires | |||
| with SAT solving, and show how to build a simple bounded model checker | |||
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. |
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
This extends the background concepts section with a description of the BMC algorithm. Review needed!
Documentation only commit: