Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:homework03 [2008/03/06 19:06] vkuncak |
sav08:homework03 [2008/03/06 19:29] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Homework 03 - DRAFT ====== | + | ====== Homework 03 ====== |
| - | ===== Problem 1: Verification Condition Generator using Symbolic Execution ===== | + | ===== Problem 1: NAND ===== |
| - | 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]]. | + | Extend propositional formulas with NAND operator, denoted $\barwedge$ and defined by |
| + | \[ | ||
| + | x \barwedge y = \lnot (x \land y) | ||
| + | \] | ||
| + | Show that for each propositional formula $F$ there exists an equivalent formula that uses $\barwedge$ as the only operator. | ||
| - | You do not need to parse program text, you can simply generate test cases by writing syntax trees. | + | ===== Problem 2: Satisfiability-Preserving Transformation to CNF ===== |
| - | Your verification condition generator should work in the presence of loops, assuming that the program is annotated with loop invariants expressed as 'assert' statements written before the loop. | + | Your goal here is to prove key steps in transformation of a formula containing $\land,\lor,\lnot$ to equisatisfiable CNF formula. The key transformation steps that introduce fresh variables for formula subtrees can be summarized as follows: |
| - | + | \[\begin{array}{l} | |
| - | Connect your program to a theorem prover to prove the verification conditions. You can | + | F\ \ \leadsto\ \ (p_i \leftrightarrow (q \land r)) \land subst(\{q \land r \mapsto p_i\},F) \\ |
| - | * feed them into the formDecider.opt prover from the [[:Jahob system]] or | + | F\ \ \leadsto\ \ (p_i \leftrightarrow (q \lor r)) \land subst(\{q \lor r \mapsto p_i\},F) \\ |
| - | * use [[SMT-LIB format]] and a prover such as CVC3 | + | F\ \ \leadsto\ \ (p_i \leftrightarrow (\lnot q)) \land subst(\{(\lnot q) \mapsto p_i\},F) \\ |
| - | + | \end{array} | |
| - | ===== Problem 2: Satisfiability-Preserving Translation to CNF ===== | + | \] |
| - | + | Note that each introduced equivalence, such as, $(p_i \leftrightarrow (q \land r))$ can generate several clauses. Suppose now that $F$ is in negation-normal form. Show that we can replace some of these equivalences with implications. Write the new transformation rules and prove that they produce equisatisfiable formulas. | |
| - | Prove correctness of polarity-based improvements for satisfyability-preserving transforming to CNF. | + | |
| ===== Problem 3: Equivalence Preserving Transformation to CNF ===== | ===== Problem 3: Equivalence Preserving Transformation to CNF ===== | ||
| Line 24: | Line 27: | ||
| 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.) | 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: Verification Condition Generator using Symbolic Execution ===== |
| - | Extend propositional formulas with NAND operator, denoted $\barwedge$ and defined by | + | 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]]. |
| - | \[ | + | |
| - | x \barwedge y = \lnot (x \land y) | + | You do not need to parse program text, you can simply generate test cases by writing syntax trees. |
| - | \] | + | |
| - | Show that for each propositional formula $F$ there exists an equivalent formula that uses $\barwedge$ as the only operator. | + | Your verification condition generator should work in the presence of loops, assuming that the program is annotated with loop invariants expressed as 'assert' statements written before the loop. |
| + | |||
| + | Connect your program to a theorem prover to prove the verification conditions. You can | ||
| + | * feed them into the formDecider.opt prover from the [[:Jahob system]] or | ||
| + | * use [[SMT-LIB format]] and a prover such as CVC3 | ||