| |
| Previous course: C4363 |
| Offered by:
Department of Information Technology
(IT) |
| No credit points with: C4363 |
| Prerequisite: 49270 |
| Desirable: 49280.49285.49363 |
| Recommended semester:
7th - 9th semester |
| Scope and form: Lectures. Problem solving. 6 mandatory assignments. |
| Examination:
Approval of compulsory activities is a prerequisite for taking part in the exam. Written exam
(13 point scale
) |
| Contact person: |
Henrik R. Andersen, IT, Building 343, Tel. +45 4525 3761 |
|
| Aim: To introduce construction and use of tools for formal verification of hardware and software. The participants will be able to use such tools for verifying small realistic examples. |
| Contents: Introduction to a few practically useful tools for formal verification of hardware and software descriptions. The construction of such tools is described to give the participants a thorough understanding of their potential and limitations. Furthermore, the participants will be trained in the use of one of the tools to enable them to use it for modeling and verification of realistic examples. The mandatory assignments include both use of the tools and doing minor modifications (in order to understand how they are constructed). |
