A. I. Cuza University of IaşiSpecification and Verification of the Systems
| Course name | Specification and Verification of the Systems | Code | MISS2101 |
| Class | Master of Software Engineering, 2007 - 2009 | ||||||
| Level | Master | Year | 2 | Semester | 1 | Status | |
| Hours per week | Total hours per semester | Total hours of individual work | Credits | Evaluation type | Teaching language | |||
| C | S | L | Pr | |||||
| 2 | 2 | 0 | 0 | 56 | 124 | 8 | M | ro |
| Taught by | Academic and scientific title, name |
|
Professor, PhD,
Dorel Lucanu
|
| Required courses |
| Objectives | Insusirea and understanding of the concepts and techniques of specification and verification systems. |
| General thematics | Specification, verification and test-based model: Spec #, AsmL, SpecExplorer, Model Checking. Static code analysis: splint, Ccecured ... Automatic demonstration: Isabelle, Coq, Maud ... |
| Seminary / Laboratory thematics | Individual work for projects consisting of the specification and verification systems in the real world. Referate. |
| Teaching methods | Lectures on the system using videoproiectorul interactive presentations and debate projects. |
| Bibliography | SpecExplorer home page: http://research.microsoft.com/projects/specexplorer/ EMClarke, O. Grumberg, D. Peled: `` Model Checking'', MIT Press, 1999 Spin home page: http://spinroot. com / spin / whatispin.html Splint home page: http://splint.org/ |
| Evaluation | conditions | Activity in the seminar (presentation projects). Written exam. |
| criterias | Each condition must be fulfilled to obtain at least a grade 5 (or equivalent) | |
| modes | Activity in the workshop (60%), written exam (40%), presentation of reports is a bonus. If the bonus is significant, may replace one of the other activities. | |
| formula | Activity laboratory examination x 0.6 x 0.4 + + Referate |