Teachers: Prof. Stavros Tripakis
Status of the Course:
Compulsory course of the Algorithms, Logic and Computation track (Master's level).
Level of the Course:
III - IV (Spring 2018)
There will be approximately 16 lectures of 2 hours each, biweekly homeworks, a final exam, and a project.
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+.
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:
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.
Slides, lecture notes, and research papers provided during class
Substitutes for Courses:
ICS-E5010 Computer-Aided Verification and Synthesis
Bachelor degree in computer science (or equivalent) recommended. Undergraduates wishing to attend are asked to email Prof. Tripakis prior to registering.
Language of Instruction:
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.