Topic outline

  • 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.