|
The exam will cover the first 14 lectures, up through verification condition generation. The following give examples of the kinds of questions you are likely to be asked for each topic:
- Propositional Logic
- Determine whether a proposition is satisfiable or valid in the standard model.
- Give a proof of a proposition using the Natural Deduction proof system for propositional logic.
- Come up with proof rules for new propositional connectives.
- First-Order Logic
- Read and understand a signature for first-order formulae.
- Determine whether a formula is satisfied by a given assignment, or give an assignment that satisfies or falsifies the formula.
- Find the free variables of a term.
- Prove that a proposition is valid, or come up with proof rules for a new first-order construct.
- Hoare Logic
- Give proofs for Hoare triples.
- Provide loop invariants that can be used to verify Hoare triples for programs.
- Come up with proof rules for new language constructs.
- Verification Condition Generation
- Find weakest preconditions for programs given post-conditions.
- Calculate verification conditions for programs and post-conditions or for Hoare triples.
|