Fiches de cours 2017-2018

PDF
 

Synthesis, analysis and verification

CS-550

Lecturer(s) :

Language:

English

Remarque

pas donné en 2017-18

Summary

The course presents theory, algorithms, and tools for reasoning about computer systems, including techniques for software and hardware verification and synthesis.

Content

Motivation:
Tools for automated analysis and verification of software can improve reliability of software that we use every day. The underlying techniques are also used for compiler optimizations and program understanding. In recent years, new algorithms and combinations of existing techniques have made such tools more effective than in the past. This course will give an overview of basic techniques, as well as the recent advances that made this progress possible.

In many years the course also contains guest lectures presenting recent research results.

Topics covered include:

Learning Prerequisites

Required courses

Theoretical computer science and discrete mathematics course, or equivalent background and fluency in discrete mathematics and introductory theoretical computer science concepts (e.g. M. Sipser textbook)

Functional programming in Scala, or ability to pick up Scala quickly (students knowing Haskell or ML generally have no trouble).

Recommended courses

The knowledge of mathematical logic and combinatorial optimization is beneficial

Learning Outcomes

By the end of the course, the student must be able to:

Transversal skills

Teaching methods

Ex catedra

Exercise sessions

Practical work on projects under supervision of teaching assistants

Expected student activities

Attending lectures

Exercises in class

Homeworks

Mid-term exam

Practical project on modifying a verification system

Assessment methods

Supervision

Office hours Yes
Assistants Yes
Forum Yes

Resources

Bibliography

The Calculus of Computation: Decision Procedures with Applications to Verification. Bradley, Aaron R., Manna, Zohar, Springer, 2007. ISBN 978-3-540-74113-8.

Ressources en bibliothèque
Notes/Handbook

http://lara.epfl.ch/w/sav13:top

Websites
Videos

In the programs

  • Computer Science, 2017-2018, Master semester 2
    • Semester
      Spring
    • Exam form
      During the semester
    • Credits
      6
    • Subject examined
      Synthesis, analysis and verification
    • Lecture
      2 Hour(s) per week x 14 weeks
    • Exercises
      2 Hour(s) per week x 14 weeks
    • Project
      2 Hour(s) per week x 14 weeks
  • Communication Systems - master program, 2017-2018, Master semester 2
    • Semester
      Spring
    • Exam form
      During the semester
    • Credits
      6
    • Subject examined
      Synthesis, analysis and verification
    • Lecture
      2 Hour(s) per week x 14 weeks
    • Exercises
      2 Hour(s) per week x 14 weeks
    • Project
      2 Hour(s) per week x 14 weeks
  • Communication Systems - master program, 2017-2018, Master semester 4
    • Semester
      Spring
    • Exam form
      During the semester
    • Credits
      6
    • Subject examined
      Synthesis, analysis and verification
    • Lecture
      2 Hour(s) per week x 14 weeks
    • Exercises
      2 Hour(s) per week x 14 weeks
    • Project
      2 Hour(s) per week x 14 weeks
  • Computer engineering minor, 2017-2018, Spring semester
    • Semester
      Spring
    • Exam form
      During the semester
    • Credits
      6
    • Subject examined
      Synthesis, analysis and verification
    • Lecture
      2 Hour(s) per week x 14 weeks
    • Exercises
      2 Hour(s) per week x 14 weeks
    • Project
      2 Hour(s) per week x 14 weeks
  • Computer and Communication Sciences (edoc), 2017-2018
    • Semester
      Spring
    • Exam form
      During the semester
    • Credits
      6
    • Subject examined
      Synthesis, analysis and verification
    • Lecture
      2 Hour(s) per week x 14 weeks
    • Exercises
      2 Hour(s) per week x 14 weeks
    • Project
      2 Hour(s) per week x 14 weeks

Reference week

MoTuWeThFr
8-9
9-10
10-11
11-12
12-13
13-14
14-15
15-16
16-17
17-18
18-19
19-20
20-21
21-22
Lecture
Exercise, TP
Project, other

legend

  • Autumn semester
  • Winter sessions
  • Spring semester
  • Summer sessions
  • Lecture in French
  • Lecture in English
  • Lecture in German