Credits: 5

Schedule: 03.01.2018 - 29.03.2018

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): 

0-5

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.

Description