(Formal Verification)A very short introduction to Model Checking and Program Verification
Department of Mathematical Sciences
Formal verification is the act of proving or disproving the correctness of intended (hardware or software) systems. A Formal verification technique consists of following three stages.
Description: A framework to make formal Descriptions of computer systems.
Specification: A language to provide Specifications of the properties to be verified.
Verification: A Verification method to establish whether the description of a system satisfies the specification.
There are roughly two approaches to formal verification:
In theorem proving approach, the system description is a set of formulas Γ (in a suitable logic), and the specification is another formula φ. The verification method consists of trying to logically infer φ from Γ.
model checking approach, the system description is a model M for an
appropriate logic, and the specification is again a formula φ. The
verification method consists of computing whether a model M
|Course Grade: Your course grade will be determined by a combination of the following factors: 1. Students project (15%), 2. Students tasks (15%), and 3. final exam (70%). Students tasks will typically be handed in the lecture notes, and should be back in a week. Late tasks will not be accepted unless a permission is obtained in advance.|