Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:homework03 [2008/03/06 17:51] vkuncak |
sav08:homework03 [2008/03/06 19:06] vkuncak |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Problem 1: Verification Condition Generator using Symbolic Execution ===== | ===== Problem 1: Verification Condition Generator using Symbolic Execution ===== | ||
| - | Build a verification condition generator based on forward symbolic execution, extending [[homework02#Problem 4]] and using the description of [[Forward Symbolic Execution]] from [[lecture05]]. | + | Build a verification condition generator based on forward symbolic execution, extending [[homework02#Problem 4]] from [[homework02]] and using the description of [[Forward Symbolic Execution]] from [[lecture05]]. |
| You do not need to parse program text, you can simply generate test cases by writing syntax trees. | You do not need to parse program text, you can simply generate test cases by writing syntax trees. | ||
| Line 22: | Line 22: | ||
| in conjunctive normal form. You do not need to use any deep results of complexity theory. | in conjunctive normal form. You do not need to use any deep results of complexity theory. | ||
| - | Specifically, prove that there exists an infinite family of formulas $F_1, F_2,\ldots$ such that for each $n$ //any// algorithm that transforms $F_n$ to CNF needs exponential time. (Note that it is not enough to prove that one particular algorithm will take exponential time, you need to prove that every algorithm would need exponential time.) | + | Specifically, prove that there exists an infinite family of formulas $F_1, F_2,\ldots$ such that for each $n$, //every// algorithm that transforms $F_n$ to CNF needs exponential time. (Note that it is not enough to prove that one particular algorithm will take exponential time, you need to prove that every algorithm would need exponential time.) |
| ===== Problem 4: NAND ===== | ===== Problem 4: NAND ===== | ||