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.