CS-E4520 - Computer-Aided Verification and Synthesis, 07.01.2019-11.04.2019
Kurssiasetusten perusteella kurssi on päättynyt 11.04.2019 Etsi kursseja: CS-E4520
Osion kuvaus
-
Credits: 5
Teachers: Prof. Stavros Tripakis
Status of the Course:
Compulsory course of the Algorithms, Logic and Computation track (Master's level).
Level of the Course:
Master’s level
Teaching Period:
III - IV (Spring 2019)
Workload:
There will be approximately 16 lectures of 2 hours each, biweekly homeworks, a final exam, and a project.
Learning Outcomes:
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 solver Z3, the theorem prover Coq, and synthesis tools such as Acacia+.
Content:
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. We will also cover the fundamentals of logic and theorem proving using the Coq proof assistant.
Assessment Methods and Criteria:
The grade will be based on class participation (20%), homeworks (40%), and final exam (40%). Optional project for Spring 2018, will get you bonus points and improve your grade.
Study Material:
Slides, lecture notes, and research papers provided during class
Substitutes for Courses:
ICS-E5010 Computer-Aided Verification and Synthesis
Prerequisites:
Bachelor degree in computer science (or equivalent) may be useful, but not strictly required.
Grading Scale:
0-5
Language of Instruction:
English
Further Information:
The course is open to all: masters students, PhD students, postdocs, and undergraduates.