Credits: 5
SCHEDULE
| Date and time | Place |
|---|
Contact information for the course (applies in this implementation):
The instructor (Prof. Tripakis) and any occasional teaching assistants will always be available to arrange appointments by email. Regular office hours may be arranged also in class depending on student interest.
Teaching Period (valid 01.08.2018-31.07.2020):
III - IV (Spring)
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.
Details on the course content (applies in this implementation):
There are some changes from year to year: prospective students are advised to look at the front page of the course in mycourses for the most updated version of the contents.
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%).
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.
Additional information for the course (applies in this implementation):
The course is open to everyone, including undergraduates, masters, PhD students, and postdocs.