Introduction to the techniques and tools for automatic verification of hardware and software
Modeling of hardware and software, overview of computer aided verification methods. Specification by temporal logic and automata, state explosion, explicit model checking, symbolic model checking with BDDs, bounded model checking with SAT, abstraction. Modeling and specification languages (Promela, SMV, TLA+). Verification software in practice (Spin, NuSMV, TLC), overview of verification methods for specific classes of systems and current developments.
Registration about TISS Students of Studies 931, 938 are prefered. Please, subscribe the lecture. Dates for lecture hall are for 181.144 and 181.145.
ECTS Breakdown:----------------------------------25h lectures and examination35h preparation for examination15h exercises----------------------------------75h (3 ECTS)----------------------------------
The students will do exercises the course. Examination score is 20% of the score for the exercises and 80% of the score for the examination questions.
aktuelle Infos bitte LVA abonnieren Ort: TISS
Bachelor in Computer Science/Informatics or related fields. It is recommended to attend this course after Formal Methods in Computer Science (185.291), as topics such as temporal logics are covered in less detail in the CAV lectures.