ADVANCED LOGIC

 (Formal Verification)

A very short introduction to Model Checking and Program Verification

Department of Mathematical Sciences

Rasool Ramezanian





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:
1. Theorem Proving
2. Model Checking

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 Γ.

In 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 satisfies φ.























 
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.