After successful completion of the course, students are able to
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). Verification software in practice (Spin, NuSMV), overview of verification methods for specific classes of systems and current developments.
The course is composed of 6 (blocked) lectures, which will take place online via Zoom.
Registration about TISS Students of Studies 931, 938 are prefered. Please, subscribe the lecture.
ECTS Breakdown:----------------------------------25h lectures and examination35h preparation for examination15h exercises----------------------------------75h (3 ECTS)----------------------------------
The course will have a written exam. The date of the final written exam will be announced later. The exam will be an open-book exam.
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.