Schedule: 02.01.2017 - 30.03.2017
Teaching Period (valid 01.08.2018-31.07.2020):
III - IV (Spring) Course removed from course selection. Contact person Prof. Petteri Kaski.
Learning Outcomes (valid 01.08.2018-31.07.2020):
The students will learn how to formally model and specify systems and their properties, and the fundamental techniques and algorithms for checking automatically that a system satisfies a property, as well as for synthesizing automatically systems that satisfy certain properties by construction. The students will be exposed to state-of-the-art verification tools such as the model-checkers NuSMV and Spin, the SAT and SMT solvers Minisat and Z3, the theorem provers PVS and Isabelle, and synthesis tools such as Acacia+.
Content (valid 01.08.2018-31.07.2020):
Designing large and complex systems (digital circuits, embedded control systems such as automated vehicles, computerized health-care devices such as pacemakers, cyber-physical systems such as automated intersections, etc.) cannot be done “by hand”. Instead, designers use computer-aided techniques, that allow to build system models (”virtual systems”) and verify correctness of the design before the real system is actually built. This course covers fundamental topics in computer-aided verification, including modeling and specification formalisms, transition systems and temporal logic, regular and omega-regular languages, safety and liveness properties, state-space exploration, model checking, SAT solving, bounded-model checking, binary-decision diagrams, compositionality and assume-guarantee reasoning, contracts and component-based design. The course also covers fundamental topics in computer-aided synthesis of correct-by-construction systems, starting from high-level formal specifications, or from example scenarios.
Assessment Methods and Criteria (valid 01.08.2018-31.07.2020):
The grade will be based on class participation (10%), homeworks (30%), final exam (40%), and the project (20%).
Workload (valid 01.08.2018-31.07.2020):
There will be approximately 16 lectures of 2 hours each, biweekly homeworks, a final exam, and a project.
Study Material (valid 01.08.2018-31.07.2020):
Slides, lecture notes, and research papers provided during class
Substitutes for Courses (valid 01.08.2018-31.07.2020):
ICS-E5010 Computer-Aided Verification and Synthesis
Prerequisites (valid 01.08.2018-31.07.2020):
Bachelor degree in computer science (or equivalent) recommended. Undergraduates wishing to attend are asked to email Prof. Tripakis prior to registering.
Grading Scale (valid 01.08.2018-31.07.2020):
Further Information (valid 01.08.2018-31.07.2020):
The course is primarily for masters, and phd-level students, but may also be appropriate for advanced undergraduates. In the latter case, please check with instructor beforehand.