Formal Verification

Formal Verification deals with a class of methods used to check whether a system satisfies a given specification. It is typically applied to the verification of software and digital hardware. By means of appropriate software tools, formal verification provides a mathematical proof showing whether a system satisfies or not the specification. To verify a system, a formal representation or model of the system is needed (such as a state machine), and a formal representation of the specification (such as a set of logic formulas). Formal verification differs from verification by simulation in that the latter only verifies the system states that are simulated; nothing can be said with certainty about the states that are not simulated. Moreover, usually there is not enough time to simulate a system in every possible state with every possible input.

At LeTourneau University, ENGR6963 Formal Verification was offered during the summer of 2014. The class has focused on the verification of software, with special emphasis on the topics related to the ACTS tools. The format of the class was as follows.


Homework: Weekly homework sets were assigned. A few problems require these files.

Lectures:

  1. Introduction.
  2. Propositional logic.
  3. Propositional logic. First order logic.
  4. First order logic. Temporal logic. LTL.
  5. LTL and CTL.
  6. CTL and CTL*.
  7. CTL*. CTL versus LTL. Model checking.
  8. Model checking with CTL specifications.
  9. Model checking with LTL specifications. Buchi automata.
  10. The NuXMV tool.
  11. Binary decision diagrams (BDDs).
  12. BDDs.
  13. ACTS and NuXMV. Representing supervision in NuXMV. Converting ACTS specifications to NuXMV specifications.
  14. ACTS and NuXMV. Transition synchronization in NuXMV.
  15. Fair model checking.
  16. The SPIN tool.
  17. The SPIN tool. Fairness features.
  18. The SPIN tool. Representing supervision in SPIN.
  19. The SPIN tool. Representing supervision in SPIN.
  20. Partial order reduction.
  21. SAT solvers. Bounded model checking.
  22. The CBMC tool.
  23. Introduction to automated theorem proving. Higher order logic.
  24. Introduction to automated theorem proving.
  25. The Herbrand method.
  26. The Herbrand method. First order theorem proving.
  27. First order theorem proving.

Home