[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/final
[Index] || [Contents] || [Grades] Mon Mar 10 17:41:58 PST 2003
```656/556 2003 1w 21 Final Outline
Comprehensive: Chapters 1,2,3,4, & 6.
Final 200 points. Answer 4 out of given 5 questions each worth 50 points.

Each question can have several parts.  The following skills may be tested
Qn 1. Propositions, Normal Forms & OBDDs
Draw parse tree of a well-formed formula (wff)
Convert wff into a truthtable/OBDD.
Use a given CNF/truthtables/OBDD to verify that wff  is always true
(or an argument valid).
Use a given DNF/truthtables/OBDD/  to prove that wff can be satisfied.
Convert OBDD to Boolean Expression/Proposition
Draw the reduced Ordered Binary Decision Diagram of ....
Use the reduce and apply algorithms in the book.
Give reasons why OBDDs are an important technique for formal
methods people.
Give examples of tools that use OBDDs.

Qn 2. Predicate Calculus
Draw parse trees of given wffs of the Predicate Calculus:
Prove a given theorem (with a short proof) from the Predicate Calculus.
Translate of English to well-formed formulae of the Predicate Calculus
Translate assumptions and prove a conclusions (when proof is simple)
Explain what Prolog can be used for.

Qn 3. Model checking and CTL
Draw parse tree of well-formed formula of CTL.
Draw  a finite state model to fit a given description of states,
transitions etc..
Unwind a finite state model into a tree
Demonstrate how OBDDs can express a finite state model.
Calculate states in a model that do or do not satisfy a given CTL
formulae
Express common types of specification  in CTL.
Explain what a model checking tool like SMV or Spin  can do for a
project reported in the literature.
.
Qn 4. Verification
Push Assertions backwards though given assignments.
Generate and verify assertions involving 'if's.
Given loop invariants fill in and  verify assertions in code that
has a loop using Tableaux and proving partial correctness.
Give an example of a common program structure missing in the
texts "Core" language and show that this lets the books
methods from applying to (say)C++.
Explain when program verification can help a programmer/designer.

Qn. 5
Write a 1 page essay describing the content of any presentation --
but not one you gave.

Items covered next year
Use Shannon's Expansion to generate an OBDD
Use Boolean Algebra 01+*- to
express a proposition,  argument, or theorem
transform <>  to Conjunctive Normal Form (CNF)
transform <> to Disjunctive Normal Form (DNF)
Interpret resulting constant values of 0(inconsistent)
or 1(theorem/valid)
Given loop invariants fill in and  verify assertions in code that
has a loop using Tableaux and proving  total correctness.

```